Mercurial > hg > Members > kono > Proof > galois
changeset 263:93a2a2c2d7c0
connected
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 May 2022 11:36:57 +0900 |
| parents | f36d2ed8ed9e |
| children | c4458b479a0f |
| files | src/FundamentalHomomorphism.agda |
| diffstat | 1 files changed, 6 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda Mon May 30 11:28:38 2022 +0900 +++ b/src/FundamentalHomomorphism.agda Mon May 30 11:36:57 2022 +0900 @@ -159,7 +159,7 @@ EqG = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup (IsGroup.isMonoid (Group.isGroup G) ))) h1 : {x : Group.Carrier G } → Coset G K x → Carrier - h1 (coset a b) = f a ∙ f (sub K b) + h1 (coset a b) = f a h : CosetCarrier G K → Carrier -- G / K → H h r = h1 (isCoset r) _o_ = Group._∙_ G @@ -169,11 +169,10 @@ h13 : {gx gy : Group.Carrier G } → ( x : Coset G K gx ) ( y : Coset G K gy ) → h (Group._∙_ (G / K) record { r = gx ; isCoset = x } record {r = gy ; isCoset = y } ) ≈ h1 x ∙ h1 y h13 (coset a b) (coset c d) = begin - h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≡⟨ _≡_.refl ⟩ - f ( ((a o sub K b) o (c o sub K d)) o ( Group._⁻¹ G (sub K ((a o sub K b) o (c o sub K d))) )) ∙ - f (sub K ((a o sub K b ) o (c o sub K d))) ≈⟨ {!!} ⟩ - f ((a o sub K b ) o (c o sub K d)) ≈⟨ {!!} ⟩ - f a ∙ f (sub K b) ∙ (f c ∙ f (sub K d)) ≡⟨ _≡_.refl ⟩ + h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≡⟨ _≡_.refl ⟩ + f ( ((a o sub K b) o (c o sub K d )) o Group._⁻¹ G ( sub K ( (a o sub K b) o (c o sub K d)))) ≈⟨ {!!} ⟩ + f (a o c) ≈⟨ {!!} ⟩ + f a ∙ f c ≡⟨ _≡_.refl ⟩ h1 (coset a b) ∙ h1 (coset c d) ∎ h-homo : IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h h-homo = record { @@ -186,7 +185,7 @@ unique : (x : Group.Carrier G) → f x ≈ h ( φ x ) unique x = begin f x ≈⟨ {!!} ⟩ - f ( x o (Group._⁻¹ G (sub K x))) ∙ f (sub K x) ∎ + f ( x o (Group._⁻¹ G (sub K x))) ∎