# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1694416089 -32400
# Node ID 76c80a6ad4e66bdb1f4443260193d75bc797f654
# Parent  7ef312aa023572922284fe858df10378dfa8f1ca
...

diff -r 7ef312aa0235 -r 76c80a6ad4e6 src/Homomorphism.agda
--- a/src/Homomorphism.agda	Mon Sep 11 09:02:40 2023 +0900
+++ b/src/Homomorphism.agda	Mon Sep 11 16:08:09 2023 +0900
@@ -299,7 +299,6 @@
     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
@@ -353,12 +352,12 @@
              isGroupHomomorphism = record {
                  isMonoidHomomorphism = record {
                       isMagmaHomomorphism = record {
-                         isRelHomomorphism = record { cong = λ {x} {y} eq → ? }
-                       ; homo = ? }
-                    ; ε-homo = ? }
-                   ; ⁻¹-homo = ? }
-               ; injective = λ x → ? }
-       ;  surjective = λ nx → ? , ?
+                         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
@@ -366,6 +365,33 @@
     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   ∎