Mercurial > hg > Members > kono > Proof > galois
view src/Homomorphism.agda @ 320:8fb16f9a882a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 19 Sep 2023 11:11:38 +0900 (2023-09-19) |
parents | fff18d4a063b |
children | e9de2bfef88d |
line wrap: on
line source
{-# OPTIONS --cubical-compatible --safe #-} -- 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 -- -- 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 -- 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. -- -- 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 ⁻¹ ∎ 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 an04 = begin b ∙ n ≈⟨ car (gsym eq) ⟩ a ∙ n ≈⟨ eq1 ⟩ x ∎ aneq : {a b : Carrier } → a ≈ b → aNeq N a b -- a ≈ b → aN ≈ bN aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt } _=n=_ = aNeq N 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) } -- factor group has the same carrier as the original group -- so h = f _/_ : {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 = 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 = aneq (solve monoid) gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) 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 ) → Set (c ⊔ d) K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where open Group H open NormalSubGroup K Ker : {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 Ker {c} {d} G H {f} f-homo = record { Psub = 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 ε≈ε⁻¹ ⟩ ε ∎ 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 _ ⟩ ε ∎ 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 ) (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 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 except cong 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 ∎ -- -- Another from of Fundamental Homomorphism Theorm -- i.e. G / Ker f ≈ Im f record IsImage {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 ) (x : Group.Carrier H) : Set (c Level.⊔ d) where field gelm : Group.Carrier G x=fg : H < x ≈ f gelm > Im : {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 ) → SubGroup {c Level.⊔ d} H Im G {H} {f} f-homo = record { P = λ x → IsImage G H f-homo x ; Pε = record { gelm = Group.ε G ; x=fg = gsym ε-homo } ; P⁻¹ = λ x imx → record { gelm = Group._⁻¹ G (gelm imx) ; x=fg = im00 (x=fg imx) } ; P≈ = im01 ; P∙ = im02 } where open IsImage open Group H open Gutil H open IsGroupHomomorphism f-homo open EqReasoning (Algebra.Group.setoid H) GC = Group.Carrier G im00 : {x : Carrier } {y : GC } → x ≈ f y → x ⁻¹ ≈ f ((G Group.⁻¹) y ) im00 {x} {y} x=fy = begin x ⁻¹ ≈⟨ ⁻¹-cong x=fy ⟩ (f y) ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ f ((G Group.⁻¹) y ) ∎ im01 : {a b : Carrier} → a ≈ b → IsImage G H f-homo a → IsImage G H f-homo b im01 {a} {b} a=b ima = record { gelm = _ ; x=fg = gtrans (gsym a=b) (x=fg ima) } im02 : {a b : Carrier} → IsImage G H f-homo a → IsImage G H f-homo b → IsImage G H f-homo (a ∙ b) im02 {a} {b} isa isb = record { gelm = G < gelm isa ∙ gelm isb > ; x=fg = im03 } where im03 : a ∙ b ≈ f (G < gelm isa ∙ gelm isb > ) im03 = begin a ∙ b ≈⟨ ∙-cong (x=fg isa) (x=fg isb) ⟩ f (gelm isa ) ∙ f (gelm isb ) ≈⟨ gsym (homo _ _ ) ⟩ f (G < gelm isa ∙ gelm isb > ) ∎ im : {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 ) → (x : Group.Carrier G) → Nelm H (Im G f-homo) im G {H} {f} f-homo x = record { elm = f x ; Pelm = record { gelm = x ; x=fg = Gutil.grefl H } } FundamentalHomomorphismTheorm2 : {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 ) → IsGroupIsomorphism (GR (G / Ker G H f-homo)) (GR (SGroup H (Im G f-homo))) (im G f-homo) FundamentalHomomorphismTheorm2 G {H} {f} f-homo = record { isGroupMonomorphism = record { -- this is essentially f-homo except cong isGroupHomomorphism = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq } ; homo = homo } ; ε-homo = ε-homo } ; ⁻¹-homo = ⁻¹-homo } ; injective = λ eq → AN.ab⁻¹∈N→a=b G (Ker G H f-homo) (h06 eq) } ; surjective = λ nx → (IsImage.gelm (Nelm.Pelm nx)) , h07 nx } where open GK G (Ker G H f-homo) open Group H open Gutil H open IsGroupHomomorphism f-homo open EqReasoning (Algebra.Group.setoid H) open Nelm GC = Group.Carrier G h07 : (nx : Nelm H (Im G f-homo)) → f (IsImage.gelm (Nelm.Pelm nx)) ≈ elm nx h07 nx = gsym ( IsImage.x=fg (Nelm.Pelm nx) ) h06 : {x y : GC} → f x ≈ f y → f (G < x ∙ Group._⁻¹ G y >) ≈ ε h06 {x} {y} fx=fy = begin f (G < x ∙ Group._⁻¹ G y >) ≈⟨ homo _ _ ⟩ f x ∙ f (Group._⁻¹ G y ) ≈⟨ cdr (⁻¹-homo _) ⟩ f x ∙ f y ⁻¹ ≈⟨ car fx=fy ⟩ f y ∙ f y ⁻¹ ≈⟨ proj₂ inverse _ ⟩ ε ∎ h = f h04 : {x y : Group.Carrier G} → aNeq (Ker G H f-homo) x y → f x ≈ f y h04 {x} {y} x=y = h20 where kf : h (G < x ∙ (G Group.⁻¹) y >) ≈ ε kf = begin h (G < x ∙ (G Group.⁻¹) y >) ≈⟨ AN.a=b→ab⁻¹∈N G (Ker G H f-homo) x=y ⟩ ε ∎ h20 : f x ≈ f 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 ⟩ ε ∙ h y ≈⟨ proj₁ identity _ ⟩ h y ∎