Mercurial > hg > Members > kono > Proof > galois
changeset 304:737c66ba371f current
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 Sep 2023 10:45:37 +0900 |
| parents | 061a0fd484c3 |
| children | ff135d2ef023 |
| files | src/Homomorphism.agda |
| diffstat | 1 files changed, 71 insertions(+), 190 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Homomorphism.agda Fri Sep 08 19:20:12 2023 +0900 +++ b/src/Homomorphism.agda Sat Sep 09 10:45:37 2023 +0900 @@ -37,17 +37,14 @@ -- ↓ / -- G/K -- +-- In our case G and G / K has the same carrier set, so φ is the identity function and f = h. +-- What we need to prove is that G / K is a Group and h has congruence. +-- (x y : Carrier (G / K ) → x ≈ y → h x ≈ h y import Relation.Binary.Reasoning.Setoid as EqReasoning open GroupMorphisms --- import Axiom.Extensionality.Propositional --- postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m - -open import Data.Empty -open import Relation.Nullary - -- Set of a ∙ ∃ n ∈ N -- @@ -68,15 +65,7 @@ -- -- (aN)(bN) = a(Nb)N = a(bN)N = (ab)NN = (ab)N. -- - naN : {a x : Carrier} → IsaN N a x → Carrier - naN (an n x eq pn) = n - aaN : {a x : Carrier} → IsaN N a x → Carrier - aaN {a} (an n x eq pn) = a - PaN : {a x : Carrier} → (iax : IsaN N a x) → P (naN iax) - PaN (an n x eq pn) = pn - anaN=x : {a x : Carrier} → (ax : IsaN N a x) → a ∙ naN ax ≈ x - anaN=x (an n x eq pn) = eq - -- a =n= b → a . b ⁻¹ ∈ N + -- a =n= b ↔ a . b ⁻¹ ∈ N a=b→ab⁻¹∈N : {a b : Carrier} → (a=b : aNeq N a b) → P (a ∙ b ⁻¹) a=b→ab⁻¹∈N {a} {b} a=b with eq→ a=b (an ε a (proj₂ identity _) Pε) ... | an n .a bn=a pn = P≈ an06 (Pcomm {n} {b} pn ) where @@ -85,35 +74,33 @@ b ∙ (n ∙ b ⁻¹) ≈⟨ solve monoid ⟩ (b ∙ n ) ∙ b ⁻¹ ≈⟨ car bn=a ⟩ a ∙ b ⁻¹ ∎ - an-factor : {x y a : Carrier } → (xua : IsaN N (x ∙ y) a ) → IsaN N x (a ∙ y ⁻¹) × IsaN N y y - an-factor {x} {y} {a} (an n a1 eqa pn) = an n1 _ an02 (Pcomm pn) - , an n2 _ an03 Pε where - an04 : x ∙ y ∙ n ≈ a - an04 = eqa - -- n ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) - -- n ∙ n2 ⁻¹ ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) - -- y ∙ (n ∙ n2 ⁻¹) ∙ y ⁻¹ ≈ n1 - n1 : Carrier - n1 = y ∙ (n ∙ y ⁻¹) - n2 : Carrier - n2 = ε - an02 : x ∙ n1 ≈ a ∙ y ⁻¹ - an02 = begin - x ∙ n1 ≈⟨ grefl ⟩ - x ∙ (y ∙ (n ∙ y ⁻¹)) ≈⟨ solve monoid ⟩ - (x ∙ y ∙ n ) ∙ y ⁻¹ ≈⟨ car eqa ⟩ - a ∙ y ⁻¹ ∎ - an03 : y ∙ n2 ≈ y - an03 = proj₂ identity _ - an-comp : {x y a b : Carrier } → IsaN N x a → IsaN N y b → IsaN N (x ∙ y) (a ∙ b) - an-comp {x} {y} {a} {b} (an n1 a1 eqa p1) (an n2 a2 eqb p2) = an (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) _ an01 (P∙ (Pcomm p1) p2) where - an01 : x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) ≈ a ∙ b - an01 = begin - x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) ≈⟨ solve monoid ⟩ - (x ∙ (y ∙ y ⁻¹) ∙ n1) ∙ (y ⁻¹) ⁻¹ ∙ n2 ≈⟨ car (∙-cong (car (cdr (proj₂ inverse _))) f⁻¹⁻¹≈f ) ⟩ - (x ∙ ε ∙ n1) ∙ y ∙ n2 ≈⟨ solve monoid ⟩ - (x ∙ n1) ∙ (y ∙ n2) ≈⟨ ∙-cong eqa eqb ⟩ - a ∙ b ∎ + ab⁻¹∈N→a=b : {a b : Carrier} → P (a ∙ b ⁻¹) → aNeq N a b + ab⁻¹∈N→a=b {a} {b} parb = record { eq→ = an07 ; eq← = an09 } where + an07 : {x : Carrier} → IsaN N a x → IsaN N b x + an07 {x} (an n x eq pn) = an _ x an08 (P∙ (Pcomm parb) pn ) where + an08 : b ∙ (( b ⁻¹ ∙ ((a ∙ b ⁻¹ ) ∙ b ⁻¹ ⁻¹ ))∙ n ) ≈ x + an08 = begin + b ∙ (( b ⁻¹ ∙ ((a ∙ b ⁻¹ ) ∙ b ⁻¹ ⁻¹ ))∙ n ) ≈⟨ solve monoid ⟩ + b ∙ (( b ⁻¹ ∙ (a ∙ (b ⁻¹ ∙ b ⁻¹ ⁻¹ ))) ∙ n ) ≈⟨ cdr (car (cdr (cdr (proj₂ inverse _)))) ⟩ + b ∙ (( b ⁻¹ ∙ (a ∙ ε)) ∙ n ) ≈⟨ solve monoid ⟩ + (b ∙ b ⁻¹ ) ∙ (a ∙ n) ≈⟨ car ( proj₂ inverse _) ⟩ + ε ∙ (a ∙ n) ≈⟨ proj₁ identity _ ⟩ + a ∙ n ≈⟨ eq ⟩ + x ∎ + an09 : {x : Carrier} → IsaN N b x → IsaN N a x + an09 {x} (an n x eq pn) = an _ x an10 (P∙ (Pcomm (P⁻¹ _ parb)) pn ) where + an10 : a ∙ (( a ⁻¹ ∙ ((a ∙ b ⁻¹ ) ⁻¹ ∙ a ⁻¹ ⁻¹ ))∙ n ) ≈ x + an10 = begin + a ∙ (( a ⁻¹ ∙ ((a ∙ b ⁻¹ ) ⁻¹ ∙ a ⁻¹ ⁻¹ ))∙ n ) ≈⟨ cdr (car (cdr (car (gsym (lemma5 _ _))))) ⟩ + a ∙ (( a ⁻¹ ∙ ((b ⁻¹ ⁻¹ ∙ a ⁻¹ ) ∙ a ⁻¹ ⁻¹ ))∙ n ) ≈⟨ cdr (car (cdr (car (car f⁻¹⁻¹≈f )))) ⟩ + a ∙ (( a ⁻¹ ∙ ((b ∙ a ⁻¹ ) ∙ a ⁻¹ ⁻¹ ))∙ n ) ≈⟨ solve monoid ⟩ + a ∙ (( a ⁻¹ ∙ (b ∙ (a ⁻¹ ∙ a ⁻¹ ⁻¹ ))) ∙ n ) ≈⟨ cdr (car (cdr (cdr (proj₂ inverse _)))) ⟩ + a ∙ (( a ⁻¹ ∙ (b ∙ ε)) ∙ n ) ≈⟨ solve monoid ⟩ + (a ∙ a ⁻¹ ) ∙ (b ∙ n) ≈⟨ car ( proj₂ inverse _) ⟩ + ε ∙ (b ∙ n) ≈⟨ proj₁ identity _ ⟩ + b ∙ n ≈⟨ eq ⟩ + x ∎ + an-cong : {a b x : Carrier } → a ≈ b → IsaN N a x → IsaN N b x an-cong {a} {b} {x} eq (an n _ eq1 pn) = an n _ an04 pn where an04 : b ∙ n ≈ x @@ -121,37 +108,9 @@ b ∙ n ≈⟨ car (gsym eq) ⟩ a ∙ n ≈⟨ eq1 ⟩ x ∎ - conj : (n x : Carrier) → Carrier - conj n x = x ∙ (n ∙ x ⁻¹) - Pconj : (n x : Carrier) → P n → P (conj n x) - Pconj n x pn = Pcomm pn - aN=Na : {x n : Carrier} → x ∙ n ≈ conj n x ∙ x - aN=Na {x} {n} = gsym ( begin - (x ∙ (n ∙ x ⁻¹)) ∙ x ≈⟨ solve monoid ⟩ - (x ∙ n ) ∙ (x ⁻¹ ∙ x) ≈⟨ cdr (proj₁ inverse _) ⟩ - (x ∙ n ) ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∙ n ∎ ) - Na=aN : {x n : Carrier} → n ∙ x ≈ x ∙ conj n (x ⁻¹) - Na=aN {x} {n} = gsym ( begin - x ∙ ( x ⁻¹ ∙ (n ∙ (x ⁻¹ ) ⁻¹ ) ) ≈⟨ solve monoid ⟩ - (x ∙ x ⁻¹ ) ∙ (n ∙ (x ⁻¹) ⁻¹) ≈⟨ ∙-cong (proj₂ inverse _) (cdr f⁻¹⁻¹≈f) ⟩ - ε ∙ (n ∙ x) ≈⟨ proj₁ identity _ ⟩ - n ∙ x ∎ ) aneq : {a b : Carrier } → a ≈ b → aNeq N a b aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt } - -- this may wrong - -- aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x) → naN ia ≈ naN ib - ayxi : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → IsaN N y (x ∙ n) - ayxi {x} {y} x=y {n} pn = eq→ x=y (an n _ grefl pn) - ayxn : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → Carrier - ayxn {x} {y} x=y {n} pn = naN (ayxi x=y pn) - Payxn : {x y : Carrier} → (x=y : aNeq N x y) → {n : Carrier} → (pn : P n) → P (ayxn x=y pn) - Payxn {x} {y} x=y {n} pn with ayxi x=y pn - ... | an n₁ .((A Group.∙ x) n) x₁ pn₁ = pn₁ _=n=_ = aNeq N - anxn=yn : {x y n : Carrier } → (x=y : aNeq N x y) → (pn : P n) → x ∙ n ≈ y ∙ (ayxn x=y pn) - anxn=yn {x} {y} {n} x=y pn with ayxi x=y pn - ... | an n₁ .((A Group.∙ x) n) eq1 pn₁ = gsym eq1 nrefl : {x : Carrier} → x =n= x nrefl {x} = record { eq→ = λ {lt} ix → ix ; eq← = λ {lt} ix → ix } @@ -187,60 +146,28 @@ open AN A N open aNeq gk00 : {x y u v : Carrier } → aNeq N x y → aNeq N u v → aNeq N (x ∙ u) (y ∙ v) - gk00 {x} {y} {u} {v} x=y u=v = record { eq→ = gk01 x=y u=v ; eq← = gk01 (nsym x=y) (nsym u=v) } where - -- xN ≈ yN → uN ≈ vN → xuN ≈ xN⁻¹NuN ≈ yN⁻¹NvN ≈ yvN - gk01 : {a x y u v : Carrier} → aNeq N x y → aNeq N u v → IsaN N (x ∙ u) a → IsaN N (y ∙ v) a - gk01 {a} {x} {y} {u} {v} x=y u=v (an n z eq pn) = an gk1n z gk13 (PaN gk14) where - gk10 : IsaN N x (a ∙ u ⁻¹) - gk10 = proj₁ (an-factor (an n z eq pn)) - gk12 : IsaN N u u - gk12 = proj₂ (an-factor (an n z eq pn)) - gk14 : IsaN N _ _ - gk14 = an-comp (eq→ x=y gk10) (eq→ u=v gk12 ) - gk1n : Carrier - gk1n = naN gk14 - gk13 : (y ∙ v) ∙ gk1n ≈ a - gk13 = begin - y ∙ v ∙ gk1n ≈⟨ grefl ⟩ - y ∙ v ∙ naN gk14 ≈⟨ anaN=x gk14 ⟩ - a ∙ u ⁻¹ ∙ u ≈⟨ solve monoid ⟩ - a ∙ (u ⁻¹ ∙ u) ≈⟨ cdr ( proj₁ inverse _) ⟩ - a ∙ ε ≈⟨ solve monoid ⟩ - a ∎ + gk00 {x} {y} {u} {v} x=y u=v = gk08 where + gk09 : (x ∙ y ⁻¹ ) ∙ (y ∙ ((u ∙ v ⁻¹) ∙ y ⁻¹ )) ≈ x ∙ u ∙ (y ∙ v) ⁻¹ + gk09 = begin + (x ∙ y ⁻¹ ) ∙ (y ∙ ((u ∙ v ⁻¹) ∙ y ⁻¹ )) ≈⟨ solve monoid ⟩ + x ∙ y ⁻¹ ∙ (y ∙ (u ∙ (v ⁻¹ ∙ y ⁻¹ ))) ≈⟨ cdr (cdr (cdr ((lemma5 _ _)))) ⟩ + x ∙ y ⁻¹ ∙ (y ∙ (u ∙ (y ∙ v) ⁻¹ )) ≈⟨ solve monoid ⟩ + x ∙ ((y ⁻¹ ∙ y ) ∙ (u ∙ (y ∙ v) ⁻¹)) ≈⟨ cdr (car (proj₁ inverse _) ) ⟩ + x ∙ (ε ∙ (u ∙ (y ∙ v) ⁻¹)) ≈⟨ solve monoid ⟩ + x ∙ u ∙ (y ∙ v) ⁻¹ ∎ + gk08 : aNeq N (x ∙ u) (y ∙ v) + gk08 = ab⁻¹∈N→a=b (P≈ gk09 (P∙ (a=b→ab⁻¹∈N x=y) (Pcomm (a=b→ab⁻¹∈N u=v)) )) gkassoc : (x y z : Carrier ) → aNeq N ((x ∙ y ) ∙ z) (x ∙ (y ∙ z)) - gkassoc x y z = record { eq→ = gk04 ; eq← = gk06 } where - gk04 : {a : Carrier } → IsaN N (x ∙ y ∙ z) a → IsaN N (x ∙ (y ∙ z)) a - gk04 {a} (an n _ eq pn) = an n _ gk05 pn where - gk05 : x ∙ (y ∙ z) ∙ n ≈ a - gk05 = begin - x ∙ (y ∙ z) ∙ n ≈⟨ solve monoid ⟩ - x ∙ y ∙ z ∙ n ≈⟨ eq ⟩ - a ∎ - gk06 : {a : Carrier } → IsaN N (x ∙ (y ∙ z)) a → IsaN N (x ∙ y ∙ z) a - gk06 {a} (an n _ eq pn) = an n _ gk05 pn where - gk05 : x ∙ y ∙ z ∙ n ≈ a - gk05 = begin - x ∙ y ∙ z ∙ n ≈⟨ solve monoid ⟩ - x ∙ (y ∙ z) ∙ n ≈⟨ eq ⟩ - a ∎ + gkassoc x y z = aneq (solve monoid) gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) - gkcong⁻¹ {x} {y} x=y = record { eq→ = gk07 x=y ; eq← = gk07 (nsym x=y) } where - -- a⁻¹N ≈ (Na)⁻¹ ≈ (aN)⁻¹ ≈ (bN)⁻¹ ≈ (Nb)⁻¹ ≈ b⁻¹N - -- a ⁻¹ ∙ n ≈ ( n ⁻¹ ∙ a ) ⁻¹ ≈ ( a ∙ n₁ ) ⁻¹ ≈ ( b ∙ n₂ ) ⁻¹ ≈ ( n₃ ∙ b ) ⁻¹ ≈ b ⁻¹ ∙ n₃ - gk07 : {a x y : Carrier } → (x=y : aNeq N x y) → IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a - gk07 {a} {x} {y} x=y (an n _ eq pn) = an ((conj (ayxn x=y pj) y )⁻¹) _ gk01 (P⁻¹ _ (Pconj _ _ (Payxn x=y pj ) ) ) where - pj : P (conj (n ⁻¹) (x ⁻¹)) - pj = Pcomm (P⁻¹ _ pn) - gk01 : y ⁻¹ ∙ (conj (ayxn x=y pj) y ) ⁻¹ ≈ a - gk01 = begin - y ⁻¹ ∙ (conj (ayxn x=y pj) _ ) ⁻¹ ≈⟨ lemma5 _ _ ⟩ - ( conj (ayxn x=y pj) _ ∙ y ) ⁻¹ ≈⟨ ⁻¹-cong (gsym aN=Na) ⟩ - (y ∙ ayxn x=y pj ) ⁻¹ ≈⟨ gsym ( ⁻¹-cong ( anxn=yn x=y pj )) ⟩ - (x ∙ conj (n ⁻¹) (x ⁻¹) ) ⁻¹ ≈⟨ ⁻¹-cong (gsym Na=aN ) ⟩ - (n ⁻¹ ∙ x ) ⁻¹ ≈⟨ gsym (lemma5 _ _ ) ⟩ - x ⁻¹ ∙ (n ⁻¹) ⁻¹ ≈⟨ cdr f⁻¹⁻¹≈f ⟩ - x ⁻¹ ∙ n ≈⟨ eq ⟩ - a ∎ + gkcong⁻¹ {x} {y} x=y = ab⁻¹∈N→a=b (P≈ gk09 (Pcomm {_} {y ⁻¹ } (P⁻¹ _ ( a=b→ab⁻¹∈N x=y)))) where + gk09 : y ⁻¹ ∙ ((x ∙ y ⁻¹) ⁻¹ ∙ (y ⁻¹) ⁻¹) ≈ x ⁻¹ ∙ (y ⁻¹) ⁻¹ + gk09 = begin + y ⁻¹ ∙ ((x ∙ y ⁻¹) ⁻¹ ∙ (y ⁻¹) ⁻¹) ≈⟨ cdr (car (gsym (lemma5 _ _))) ⟩ + y ⁻¹ ∙ ((y ⁻¹ ⁻¹ ∙ x ⁻¹ ) ∙ (y ⁻¹) ⁻¹) ≈⟨ solve monoid ⟩ + (y ⁻¹ ∙ y ⁻¹ ⁻¹ ) ∙ ( x ⁻¹ ∙ (y ⁻¹) ⁻¹) ≈⟨ car (proj₂ inverse _) ⟩ + ε ∙ ( x ⁻¹ ∙ (y ⁻¹) ⁻¹) ≈⟨ solve monoid ⟩ + x ⁻¹ ∙ (y ⁻¹) ⁻¹ ∎ -- K ⊆ ker(f) K⊆ker : {c d : Level} (G H : Group c d) (K : NormalSubGroup {d} G ) (f : Group.Carrier G → Group.Carrier H ) @@ -249,70 +176,6 @@ open Group H open NormalSubGroup K -open import Function.Surjection -open import Function.Equality - -module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G ) where - open Group G - open NormalSubGroup K - open EqReasoning (Algebra.Group.setoid G) - open Gutil G - open AN G K - - gkε : Group.Carrier (G / K) - gkε = Group.ε (G / K) - - φ : Group.Carrier G → Group.Carrier (G / K ) -- a → aN - φ g = g - - φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ - φ-homo = record {⁻¹-homo = λ x → aneq grefl ; isMonoidHomomorphism = record { ε-homo = aneq grefl - ; isMagmaHomomorphism = record { homo = λ x y → aneq grefl ; isRelHomomorphism = - record { cong = λ eq → aneq eq } }}} - - - φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) - φe = record { _⟨$⟩_ = φ ; cong = gk40 } where - gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j > - gk40 {i} {j} i=j = aneq i=j - - -- inv-φ get a prepresentable element of aN - -- any element x ≈ a ∙ n is Ok, but there is no obvious one - - -- inv-φ : Group.Carrier (G / K ) → Carrier -- P (inv-ψ x) - -- inv-φ x = ra (factor x) - - -- φ-surjective : Surjective φe - -- φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → gk50 f g } - -- ; right-inverse-of = gk60 } where - -- open aNeq - -- gk50 : (f g : Group.Carrier (G / K)) → (G / K) < f ≈ g > → inv-φ f ≈ inv-φ g - -- gk50 f g f=g = ? where - -- gk52 : IsaN K g (f ∙ rn (factor f)) - -- gk52 = eq→ f=g (an (rn (factor f)) (f ∙ rn (factor f)) grefl (prn (factor f))) - -- gk51 : G < G < g ∙ ? > ≈ G < f ∙ rn (factor f) > > - -- gk51 with gk52 - -- ... | an n .((G Group.∙ f) (rn (factor f))) gn=frn pn = ? - -- gk60 : (x : Group.Carrier (G / K )) → aNeq K (φ (inv-φ x)) x - -- gk60 = ? - -- - -- gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x > - -- gk01 = ? - - -record FundamentalHomomorphism {c d : Level} (G H : Group c d ) - (f : Group.Carrier G → Group.Carrier H ) - (homo : IsGroupHomomorphism (GR G) (GR H) f ) - (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set (Level.suc c ⊔ d) where - open Group H - open GK G K - field - h : Group.Carrier (G / K ) → Group.Carrier H - h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h - is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) - → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x )) → (( x : Group.Carrier (G / K)) → h x ≈ h1 x ) - Imf : {c d : Level} (G H : Group c d) (f : Group.Carrier G → Group.Carrier H ) (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → NormalSubGroup {d} G @@ -371,6 +234,23 @@ (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → Group _ _ FactorGroup G {H} {f} f-homo = G / Imf G H f f-homo +module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G ) where + φ : Group.Carrier G → Group.Carrier (G / K ) -- a → aN + φ g = g + +record FundamentalHomomorphism {c d : Level} (G H : Group c d ) + (f : Group.Carrier G → Group.Carrier H ) + (homo : IsGroupHomomorphism (GR G) (GR H) f ) + (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set (Level.suc c ⊔ d) where + open Group H + open GK G K + field + h : Group.Carrier (G / K ) → Group.Carrier H + h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h + is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) + → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x )) → (( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + FundamentalHomomorphismTheorm : {c d : Level} (G H : Group c d) (f : Group.Carrier G → Group.Carrier H ) (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) @@ -384,7 +264,6 @@ open GK G K open Group H open Gutil H - -- open NormalSubGroup K ? open IsGroupHomomorphism f-homo open EqReasoning (Algebra.Group.setoid H) @@ -424,9 +303,11 @@ f x ≈⟨ h1-is-solution _ ⟩ h1 ( φ x ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (AN.nrefl G K) ⟩ h1 x ∎ +-- +-- Fundamental Homomorphism Theorm on G / Imf f gives another form of Fundamental Homomorphism Theorm +-- i.e. G / Imf f ≈ Ker f -