# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1694226021 -32400
# Node ID c422ae2f2d6623ee0579167d7490968de026e3bd
# Parent  ff135d2ef02362cac17fc74f71b80d7b18b1af21
...

diff -r ff135d2ef023 -r c422ae2f2d66 src/Homomorphism.agda
--- a/src/Homomorphism.agda	Sat Sep 09 10:45:47 2023 +0900
+++ b/src/Homomorphism.agda	Sat Sep 09 11:20:21 2023 +0900
@@ -176,10 +176,10 @@
   open Group H
   open NormalSubGroup K
 
-Imf : {c d : Level} (G H : Group c d)
-    (f : Group.Carrier G → Group.Carrier H )
+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 
-Imf {c} {d} G H f f-homo = record {
+Ker {c} {d} G H {f} f-homo = record {
           P = λ x → f x ≈ ε
         ; Pε = ε-homo 
         ; P⁻¹ = im01
@@ -199,12 +199,6 @@
         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) ⟩
@@ -229,10 +223,10 @@
        ε ∙ ε  ≈⟨ proj₁ identity _ ⟩
        ε ∎ 
 
-FactorGroup : {c d : Level} (G  : Group c d) {H : Group c d}
+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 ) →  Group _ _
-FactorGroup G {H} {f} f-homo = G / Imf G H f f-homo
+Im G {H} {f} f-homo = G / Ker G H f-homo
 
 module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G  ) where
     φ : Group.Carrier G → Group.Carrier (G / K )  -- a → aN
@@ -285,7 +279,7 @@
            ε ∙ h y  ≈⟨ proj₁ identity _ ⟩ 
            h y   ∎ 
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
-    h-homo = record {    -- this is essentially f-homo 
+    h-homo = record {    -- this is essentially f-homo except cong
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
              isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq  }
@@ -301,11 +295,10 @@
     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 ∎ 
 -- 
 -- Fundamental Homomorphism Theorm on G / Imf f gives another form of Fundamental Homomorphism Theorm
---    i.e.  G / Imf f ≈ Ker f
+--    i.e.  G / Ker f ≈ Im f