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

diff -r c422ae2f2d66 -r 7ef312aa0235 src/Homomorphism.agda
--- a/src/Homomorphism.agda	Sat Sep 09 11:20:21 2023 +0900
+++ b/src/Homomorphism.agda	Mon Sep 11 09:02:40 2023 +0900
@@ -179,12 +179,12 @@
 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 {
+Ker {c} {d} G H {f} f-homo = record { Psub = record {
           P = λ x → f x ≈ ε
         ; Pε = ε-homo 
         ; P⁻¹ = im01
         ; P≈ = im02
-        ; P∙ = im03
+        ; P∙ = im03 }
         ; Pcomm = im04
        } where
     open Group H
@@ -223,10 +223,48 @@
        ε ∙ ε  ≈⟨ proj₁ identity _ ⟩
        ε ∎ 
 
+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 ) →  Group _ _
-Im G {H} {f} f-homo = G / Ker G H f-homo
+    (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 > ) ∎
+
+
+
 
 module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G  ) where
     φ : Group.Carrier G → Group.Carrier (G / K )  -- a → aN
@@ -297,10 +335,37 @@
          f x ≈⟨ h1-is-solution _ ⟩
          h1 x ∎ 
 -- 
--- Fundamental Homomorphism Theorm on G / Imf f gives another form of Fundamental Homomorphism Theorm
+-- Another from of Fundamental Homomorphism Theorm 
 --    i.e.  G / Ker f ≈ Im f
 
+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 → ? }
+                       ; homo = ? }
+                    ; ε-homo = ? }
+                   ; ⁻¹-homo = ? }
+               ; injective = λ x → ? }
+       ;  surjective = λ 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
+
 
 
-
-
diff -r c422ae2f2d66 -r 7ef312aa0235 src/NormalSubGroup.agda
--- a/src/NormalSubGroup.agda	Sat Sep 09 11:20:21 2023 +0900
+++ b/src/NormalSubGroup.agda	Mon Sep 11 09:02:40 2023 +0900
@@ -54,9 +54,7 @@
 
 infixr 9 _<_∙_>
 
--- assuming Homomorphism is too strong
---
-record NormalSubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
+record SubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
    open Group A
    field                           
        P : Carrier  → Set l
@@ -64,21 +62,38 @@
        P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
        P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
        P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
+
+-- assuming Homomorphism is too strong
+--
+record NormalSubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
+   open Group A
+   field                           
+       Psub : SubGroup {l} A
        -- gN ≈ Ng
-       Pcomm : {a b : Carrier  }  → P a  →  P ( b ∙  ( a  ∙ b ⁻¹ ) )
+       Pcomm : {a b : Carrier  }  → SubGroup.P Psub a  →  SubGroup.P Psub ( b ∙  ( a  ∙ b ⁻¹ ) )
+   P : Carrier  → Set l
+   P = SubGroup.P Psub
+   Pε : P ε
+   Pε = SubGroup.Pε Psub
+   P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
+   P⁻¹ = SubGroup.P⁻¹ Psub
+   P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
+   P≈ = SubGroup.P≈ Psub
+   P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
+   P∙ = SubGroup.P∙ Psub
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup {d} A) : Set  (Level.suc c ⊔ d)  where
+record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set  (Level.suc e ⊔ (Level.suc c ⊔ d))  where
    open Group A
-   open NormalSubGroup n 
+   open SubGroup n 
    field                           
        elm : Carrier
        Pelm : P elm
 
-NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group  (Level.suc c ⊔ d)  d
-NGroup {_} {_} {A} n = record {
-      Carrier        = Nelm n
+SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group  (Level.suc e ⊔ (Level.suc c ⊔ d))  d
+SGroup {_} {_} {_} A n = record {
+      Carrier        = Nelm A n
     ; _≈_            = λ x y → elm x ≈ elm y
     ; _∙_            = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
     ; ε              = record { elm = ε ; Pelm = Pε }
@@ -94,7 +109,7 @@
        ; ⁻¹-cong   = IsGroup.⁻¹-cong ga }
    }  where
        open Group A
-       open NormalSubGroup n 
+       open SubGroup n 
        open Nelm 
        ga = Group.isGroup A