# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1694779972 -32400
# Node ID b4a3ed9301cbc867015641db8fffae3c0915e5d8
# Parent  4dd130b93b210cf9a4fe16bc3bf585af8defe3ce
...

diff -r 4dd130b93b21 -r b4a3ed9301cb src/Homomorphism.agda
--- a/src/Homomorphism.agda	Thu Sep 14 13:03:17 2023 +0900
+++ b/src/Homomorphism.agda	Fri Sep 15 21:12:52 2023 +0900
@@ -224,48 +224,6 @@
        ε ∙ ε  ≈⟨ 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 ) →  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
@@ -338,6 +296,48 @@
 -- 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)