Mercurial > hg > Members > kono > Proof > galois
view src/Homomorphism.agda @ 303:061a0fd484c3
Foundamental theorem done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 08 Sep 2023 19:20:12 +0900 |
parents | src/homomorphism.agda@3812936d52c8 |
children | 737c66ba371f |
line wrap: on
line source
{-# 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 ∎