Mercurial > hg > Members > kono > Proof > galois
changeset 303:061a0fd484c3
Foundamental theorem done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 08 Sep 2023 19:20:12 +0900 |
| parents | 3812936d52c8 |
| children | 737c66ba371f |
| files | src/Homomorphism.agda src/homomorphism.agda |
| diffstat | 2 files changed, 432 insertions(+), 392 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Homomorphism.agda Fri Sep 08 19:20:12 2023 +0900 @@ -0,0 +1,432 @@ +{-# OPTIONS --allow-unsolved-metas #-} + +-- fundamental homomorphism theorem +-- + +module Homomorphism where + +open import Level hiding ( suc ; zero ) +open import Algebra +open import Algebra.Structures +open import Algebra.Definitions +open import Algebra.Core +open import Algebra.Bundles + +open import Data.Product +open import Relation.Binary.PropositionalEquality +open import NormalSubgroup +import Gutil +import Function.Definitions as FunctionDefinitions + +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Algebra.Morphism.Structures + +open import Tactic.MonoidSolver using (solve; solve-macro) + +-- +-- Given two groups G and H and a group homomorphism f : G → H, +-- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K +-- (where G/K is the quotient group of G by K). +-- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ. +-- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms +-- +-- f +-- G --→ H +-- | / +-- φ | / h +-- ↓ / +-- G/K +-- + +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 +-- + +data IsaN {c d : Level} {A : Group c d } (N : NormalSubGroup {d} A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where + an : (n x : Group.Carrier A ) → A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x + +record aNeq {c d : Level} {A : Group c d } (N : NormalSubGroup A ) (a b : Group.Carrier A) : Set (Level.suc c ⊔ d) where + field + eq→ : {x : Group.Carrier A} → IsaN N a x → IsaN N b x + eq← : {x : Group.Carrier A} → IsaN N b x → IsaN N a x + +module AN {c d : Level} (A : Group c d) (N : NormalSubGroup {d} A ) where + open Group A + open NormalSubGroup N + open EqReasoning (Algebra.Group.setoid A) + open Gutil A + open aNeq + -- + -- (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=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 + an06 : b ∙ (n ∙ b ⁻¹) ≈ a ∙ b ⁻¹ + an06 = begin + 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 ∎ + 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 + an04 = begin + 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 } + nsym : {x y : Carrier} → x =n= y → y =n= x + nsym {x} {y} eq = record { eq→ = λ {lt} ix → eq← eq ix ; eq← = λ {lt} ix → eq→ eq ix } + ntrans : {x y z : Carrier} → x =n= y → y =n= z → x =n= z + ntrans {x} {y} {z} x=y y=z = record { eq→ = λ {lt} ix → eq→ y=z (eq→ x=y ix) + ; eq← = λ {lt} ix → eq← x=y (eq← y=z ix) } + +_/_ : {c d : Level} (A : Group c d ) (N : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) +_/_ A N = record { + Carrier = Group.Carrier A + ; _≈_ = aNeq N + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = λ x → x ⁻¹ + ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { + isEquivalence = record {refl = nrefl + ; trans = ntrans ; sym = λ a=b → nsym a=b + } + ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v } + ; assoc = gkassoc } + ; identity = (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) ) } + ; inverse = (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) + ; ⁻¹-cong = gkcong⁻¹ + } + } where + _=n=_ = aNeq N + open Group A + open NormalSubGroup N + open EqReasoning (Algebra.Group.setoid A) + open Gutil A + 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 ∎ + 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 ∎ + 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 ∎ + +-- K ⊆ ker(f) +K⊆ker : {c d : Level} (G H : Group c d) (K : NormalSubGroup {d} G ) (f : Group.Carrier G → Group.Carrier H ) + → Set (c ⊔ d) +K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where + 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 +Imf {c} {d} G H f f-homo = record { + P = λ x → f x ≈ ε + ; Pε = ε-homo + ; P⁻¹ = im01 + ; P≈ = im02 + ; P∙ = im03 + ; Pcomm = im04 + } where + open Group H + open Gutil H + open IsGroupHomomorphism f-homo + open EqReasoning (Algebra.Group.setoid H) + + GC = Group.Carrier G + im01 : (a : Group.Carrier G) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε + im01 a fa=e = begin + f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ + f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ + ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ + ε ∎ + im00 : (a : GC) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε + im00 a fa=e = begin + f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ + f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ + ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ + ε ∎ + im02 : {a b : GC} → G < a ≈ b > → f a ≈ ε → f b ≈ ε + im02 {a} {b} a=b fa=e = begin + f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩ + f a ≈⟨ fa=e ⟩ + ε ∎ where + open import Gutil G as GU + im04 : {a b : Group.Carrier G} → f a ≈ ε → + f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε + im04 {a} {b} fa=e = begin + f ( G < b ∙ G < a ∙ (G Group.⁻¹) b > > ) ≈⟨ homo _ _ ⟩ + f b ∙ f ( G < a ∙ (G Group.⁻¹) b > ) ≈⟨ cdr (homo _ _) ⟩ + f b ∙ ( f a ∙ f ((G Group.⁻¹) b )) ≈⟨ cdr (cdr (⁻¹-homo _)) ⟩ + f b ∙ ( f a ∙ f b ⁻¹ ) ≈⟨ cdr (car fa=e) ⟩ + f b ∙ ( ε ∙ f b ⁻¹ ) ≈⟨ solve monoid ⟩ + f b ∙ f b ⁻¹ ≈⟨ proj₂ inverse _ ⟩ + ε ∎ + im03 : {a b : Group.Carrier G} → f a ≈ ε → f b ≈ ε → + f ((G Group.∙ a) b) ≈ ε + im03 {a} {b} fa=e fb=e = begin + f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩ + f a ∙ f b ≈⟨ ∙-cong fa=e fb=e ⟩ + ε ∙ ε ≈⟨ proj₁ identity _ ⟩ + ε ∎ + +FactorGroup : {c d : Level} (G : Group c d) {H : Group c d} + {f : Group.Carrier G → Group.Carrier H } + (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → Group _ _ +FactorGroup G {H} {f} f-homo = G / Imf G H f f-homo + +FundamentalHomomorphismTheorm : {c d : Level} (G H : Group c d) + (f : Group.Carrier G → Group.Carrier H ) + (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) + (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f f-homo K kf +FundamentalHomomorphismTheorm {c} {d} G H f f-homo K kf = record { + h = h + ; h-homo = h-homo + ; is-solution = is-solution + ; unique = unique + } where + open GK G K + open Group H + open Gutil H + -- open NormalSubGroup K ? + open IsGroupHomomorphism f-homo + open EqReasoning (Algebra.Group.setoid H) + + + h : Group.Carrier (G / K ) → Group.Carrier H + h r = f r + h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y + h03 x y = homo _ _ + h04 : {x y : Group.Carrier G} → aNeq K x y → h x ≈ h y + h04 {x} {y} x=y = h20 where + h20 : h x ≈ h y + h20 = begin + h x ≈⟨ gsym (proj₂ identity _) ⟩ + h x ∙ ε ≈⟨ cdr (gsym (proj₁ inverse _)) ⟩ + h x ∙ ((h y) ⁻¹ ∙ h y) ≈⟨ solve monoid ⟩ + (h x ∙ (h y) ⁻¹ ) ∙ h y ≈⟨ gsym (car (cdr (⁻¹-homo _ ))) ⟩ + (h x ∙ h (Group._⁻¹ G y )) ∙ h y ≈⟨ gsym (car (homo _ _)) ⟩ + h (G < x ∙ (Group._⁻¹ G y ) > ) ∙ h y ≈⟨ car ( kf _ (AN.a=b→ab⁻¹∈N G K x=y )) ⟩ + ε ∙ h y ≈⟨ proj₁ identity _ ⟩ + h y ∎ + h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h + h-homo = record { -- this is essentially f-homo + isMonoidHomomorphism = record { + isMagmaHomomorphism = record { + isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq } + ; homo = h03 } + ; ε-homo = ε-homo } + ; ⁻¹-homo = ⁻¹-homo } + is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) + is-solution x = begin + f x ≈⟨ grefl ⟩ + h ( φ x ) ∎ + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-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 ) + unique h1 h1-homo h1-is-solution x = begin + h x ≈⟨ grefl ⟩ + f x ≈⟨ h1-is-solution _ ⟩ + h1 ( φ x ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (AN.nrefl G K) ⟩ + h1 x ∎ + + + + + +
--- a/src/homomorphism.agda Thu Sep 07 11:45:11 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,392 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} - --- fundamental homomorphism theorem --- - -module homomorphism where - -open import Level hiding ( suc ; zero ) -open import Algebra -open import Algebra.Structures -open import Algebra.Definitions -open import Algebra.Core -open import Algebra.Bundles - -open import Data.Product -open import Relation.Binary.PropositionalEquality -open import NormalSubgroup -import Gutil -import Function.Definitions as FunctionDefinitions - -import Algebra.Morphism.Definitions as MorphismDefinitions -open import Algebra.Morphism.Structures - -open import Tactic.MonoidSolver using (solve; solve-macro) - --- --- Given two groups G and H and a group homomorphism f : G → H, --- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K --- (where G/K is the quotient group of G by K). --- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ. --- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms --- --- f --- G --→ H --- | / --- φ | / h --- ↓ / --- G/K --- - -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 --- - -data IsaN {c d : Level} {A : Group c d } (N : NormalSubGroup {d} A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where - an : (n x : Group.Carrier A ) → A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x - -record aNeq {c d : Level} {A : Group c d } (N : NormalSubGroup A ) (a b : Group.Carrier A) : Set (Level.suc c ⊔ d) where - field - eq→ : {x : Group.Carrier A} → IsaN N a x → IsaN N b x - eq← : {x : Group.Carrier A} → IsaN N b x → IsaN N a x - -module AN {c d : Level} (A : Group c d) (N : NormalSubGroup {d} A ) where - open Group A - open NormalSubGroup N - open EqReasoning (Algebra.Group.setoid A) - open Gutil A - open aNeq - -- - -- (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 - 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 - 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 ∎ - 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 - an04 = begin - 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₁ - 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 - -_/_ : {c d : Level} (A : Group c d ) (N : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) -_/_ A N = record { - Carrier = Group.Carrier A - ; _≈_ = aNeq N - ; _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = λ x → x ⁻¹ - ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = nrefl - ; trans = ntrans ; sym = λ a=b → nsym a=b - } - ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v } - ; assoc = gkassoc } - ; identity = (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) ) } - ; inverse = (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) - ; ⁻¹-cong = gkcong⁻¹ - } - } where - _=n=_ = aNeq N - open Group A - open NormalSubGroup N - open EqReasoning (Algebra.Group.setoid A) - open Gutil A - open AN A N - open aNeq - nrefl : {x : Carrier} → x =n= x - nrefl {x} = record { eq→ = λ {lt} ix → ix ; eq← = λ {lt} ix → ix } - nsym : {x y : Carrier} → x =n= y → y =n= x - nsym {x} {y} eq = record { eq→ = λ {lt} ix → eq← eq ix ; eq← = λ {lt} ix → eq→ eq ix } - ntrans : {x y z : Carrier} → x =n= y → y =n= z → x =n= z - ntrans {x} {y} {z} x=y y=z = record { eq→ = λ {lt} ix → eq→ y=z (eq→ x=y ix) - ; eq← = λ {lt} ix → eq← x=y (eq← y=z ix) } - 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 ∎ - 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 ∎ - 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 ∎ - --- K ⊂ ker(f) -K⊆ker : {c d : Level} (G H : Group c d) (K : NormalSubGroup {d} G ) (f : Group.Carrier G → Group.Carrier H ) - → Set (c ⊔ d) -K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where - 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-φ : Group.Carrier (G / K ) → Carrier -- P (inv-ψ x) - inv-φ x = x - - φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → gk50 f g } - ; right-inverse-of = gk60 } where - gk50 : (f g : Group.Carrier (G / K)) → (G / K) < f ≈ g > → inv-φ f ≈ inv-φ g - gk50 f g f=g = ? - 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 ( GK.φ G K 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 ( GK.φ G K 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 ) - (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f f-homo K kf -FundamentalHomomorphismTheorm {c} {d} G H f f-homo K kf = record { - h = h - ; h-homo = h-homo - ; is-solution = is-solution - ; unique = unique - } where - -- open GK G K - open Group H - open Gutil H - -- open NormalSubGroup K ? - open IsGroupHomomorphism f-homo - open EqReasoning (Algebra.Group.setoid H) - - Imf : NormalSubGroup G - Imf = record { - P = λ x → f x ≈ ε - ; Pε = ε-homo - ; P⁻¹ = im01 - ; P≈ = im02 - ; P∙ = im03 - ; Pcomm = im04 - } where - open NormalSubGroup K - GC = Group.Carrier G - im01 : (a : Group.Carrier G) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε - im01 a fa=e = begin - f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ - f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ - ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ - ε ∎ - im00 : (a : GC) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε - im00 a fa=e = begin - f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ - f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ - ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ - ε ∎ - im02 : {a b : GC} → G < a ≈ b > → f a ≈ ε → f b ≈ ε - im02 {a} {b} a=b fa=e = begin - f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩ - f a ≈⟨ fa=e ⟩ - ε ∎ where - open import Gutil G as GU - im04 : {a b : Group.Carrier G} → f a ≈ ε → - f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε - im04 {a} {b} fa=e = begin - f ( G < b ∙ G < a ∙ (G Group.⁻¹) b > > ) ≈⟨ homo _ _ ⟩ - f b ∙ f ( G < a ∙ (G Group.⁻¹) b > ) ≈⟨ cdr (homo _ _) ⟩ - f b ∙ ( f a ∙ f ((G Group.⁻¹) b )) ≈⟨ cdr (cdr (⁻¹-homo _)) ⟩ - f b ∙ ( f a ∙ f b ⁻¹ ) ≈⟨ cdr (car fa=e) ⟩ - f b ∙ ( ε ∙ f b ⁻¹ ) ≈⟨ solve monoid ⟩ - f b ∙ f b ⁻¹ ≈⟨ proj₂ inverse _ ⟩ - ε ∎ - im03 : {a b : Group.Carrier G} → f a ≈ ε → f b ≈ ε → - f ((G Group.∙ a) b) ≈ ε - im03 {a} {b} fa=e fb=e = begin - f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩ - f a ∙ f b ≈⟨ ∙-cong fa=e fb=e ⟩ - ε ∙ ε ≈⟨ proj₁ identity _ ⟩ - ε ∎ - - h05 : Group _ _ - h05 = G / Imf - - h : Group.Carrier (G / K ) → Group.Carrier H - h r = f r - h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y - h03 x y = homo _ _ - h04 : {x y : Group.Carrier G} → aNeq K x y → h x ≈ h y - h04 {x} {y} x=y = ? - h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h - h-homo = record { - isMonoidHomomorphism = record { - isMagmaHomomorphism = record { - isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq } - ; homo = h03 } - ; ε-homo = ε-homo } - ; ⁻¹-homo = ⁻¹-homo } - is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ ? ? x ) - is-solution x = begin - f x ≈⟨ ? ⟩ - h ( GK.φ ? ? x ) ∎ - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) - → ( (x : Group.Carrier G) → f x ≈ h1 ( GK.φ ? ? x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) - unique h1 h1-homo h1-is-solution x = begin - h x ≈⟨ grefl ⟩ - f ( GK.inv-φ ? ? x ) ≈⟨ h1-is-solution _ ⟩ - h1 ( GK.φ ? ? ( GK.inv-φ ? ? x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (GK.gk01 ? ? x) ⟩ - h1 x ∎ - - - - - -