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

diff -r 7c1e3e0be315 -r c9fbb0096224 src/homomorphism.agda
--- a/src/homomorphism.agda	Sun Sep 03 18:29:54 2023 +0900
+++ b/src/homomorphism.agda	Tue Sep 05 08:56:07 2023 +0900
@@ -50,7 +50,7 @@
 --
 
 data IsaN  {A : Group c d }  (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
-    an : (n : Group.Carrier A ) →  (pn : NormalSubGroup.P N n) → IsaN N a (A < a ∙ n > )
+    an : (n x : Group.Carrier A ) →  A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x
 
 record aNeq {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
     field
@@ -62,6 +62,45 @@
     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.
+    --
+    naN : {a x : Carrier} → IsaN N a x → Carrier
+    naN (an n x eq pn) = n
+    PaN : {a x : Carrier} → (iax : IsaN N a x) → P (naN iax)
+    PaN (an n x eq pn) = pn
+    anaN=x : {a x : Carrier} → (ax : IsaN N a x) → a ∙ naN ax ≈ x
+    anaN=x (an n x eq pn) = eq
+    an-factor : {x y a : Carrier } → (xua : IsaN N (x ∙ y) a ) → IsaN N x (a ∙ y ⁻¹) × IsaN N y y
+    an-factor {x} {y} {a} (an n a1 eqa pn) = an n1 _ an02 (Pcomm pn) 
+                  , an n2 _ an03 Pε where
+        an04 : x ∙ y ∙ n  ≈ a 
+        an04 = eqa
+        -- n ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)
+        -- n ∙ n2 ⁻¹ ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) 
+        -- y ∙ (n ∙ n2 ⁻¹) ∙ y ⁻¹  ≈ n1 
+        n1 : Carrier
+        n1 = y ∙ (n ∙ y ⁻¹)
+        n2 : Carrier
+        n2 = ε
+        an02 : x ∙ n1  ≈ a ∙ y ⁻¹
+        an02 = begin
+           x ∙ n1 ≈⟨ grefl ⟩
+           x ∙ (y ∙ (n ∙ y ⁻¹))  ≈⟨ solve monoid  ⟩
+           (x ∙ y ∙ n ) ∙ y ⁻¹  ≈⟨ car eqa  ⟩
+           a ∙ y ⁻¹ ∎
+        an03 : y ∙ n2  ≈ y
+        an03 = proj₂ identity _
+    an-comp : {x y a b : Carrier } → IsaN N x a →  IsaN N y b → IsaN N (x ∙ y) (a ∙ b)
+    an-comp {x} {y} {a} {b} (an n1 a1 eqa p1) (an n2 a2 eqb p2) = an  (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) _ an01  (P∙ (Pcomm p1) p2) where
+        an01 : x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)  ≈ a ∙ b
+        an01 = begin
+           x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)  ≈⟨ solve monoid ⟩
+           (x ∙ (y ∙ y ⁻¹) ∙ n1) ∙ (y ⁻¹) ⁻¹  ∙ n2  ≈⟨ car (∙-cong (car (cdr (proj₂ inverse _))) f⁻¹⁻¹≈f ) ⟩
+           (x ∙ ε ∙ n1) ∙ y  ∙ n2  ≈⟨ solve monoid ⟩
+           (x ∙ n1) ∙ (y ∙ n2)  ≈⟨ ∙-cong eqa eqb ⟩
+           a ∙ b  ∎
 
 _/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
@@ -72,9 +111,9 @@
     ; _⁻¹      = λ x → x ⁻¹
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
        isEquivalence = record {refl = nrefl
-           ; trans = ? ; sym = λ a=b → ? 
+           ; trans = ntrans ; sym = λ a=b → nsym a=b 
           }
-       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
+       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v }
        ; assoc = ? }
        ; identity =  ?   }
        ; inverse   =  (λ x → ? ) , (λ x → ? ) 
@@ -87,9 +126,52 @@
        open EqReasoning (Algebra.Group.setoid A)
        open Gutil A
        open AN A N
+       open aNeq 
        nrefl :  {x : Carrier} → x =n= x
-       nrefl = ?
-
+       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) }
+       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 = record { eq→ = gk01 ; eq← =  gk02 } where
+           gk01 : {a : Carrier} → IsaN N (x ∙ u) a → IsaN N (y ∙ v) a
+           gk01 {a} (an n z eq pn) = an gk1n z gk13 (PaN gk14) where
+              gk10 : IsaN N x (a ∙ u ⁻¹)
+              gk10 = proj₁ (an-factor (an n z eq pn))
+              gk12 : IsaN N u u
+              gk12 = proj₂ (an-factor (an n z eq pn))
+              gk14 : IsaN  N _ _
+              gk14 = an-comp (eq→ x=y gk10) (eq→ u=v gk12 )
+              gk1n : Carrier
+              gk1n = naN gk14
+              gk13 : (y ∙ v) ∙ gk1n  ≈ a
+              gk13 = begin
+                 y ∙ v ∙ gk1n  ≈⟨ grefl ⟩ 
+                 y ∙ v ∙ naN gk14  ≈⟨ anaN=x gk14 ⟩ 
+                 a ∙ u ⁻¹ ∙ u  ≈⟨ solve monoid ⟩ 
+                 a ∙ (u ⁻¹ ∙ u)  ≈⟨ cdr ( proj₁ inverse _)  ⟩ 
+                 a ∙ ε  ≈⟨ solve monoid  ⟩ 
+                 a ∎
+           gk02 : {a : Carrier} → IsaN N (y ∙ v) a → IsaN N (x ∙ u) a
+           gk02 {a} (an n z eq pn) = an gk1n z gk13 (PaN gk14) where
+              gk10 : IsaN N y (a ∙ v ⁻¹)
+              gk10 = proj₁ (an-factor (an n z eq pn))
+              gk12 : IsaN N v v
+              gk12 = proj₂ (an-factor (an n z eq pn))
+              gk14 : IsaN  N _ _
+              gk14 = an-comp (eq← x=y gk10) (eq← u=v gk12 )
+              gk1n : Carrier
+              gk1n = naN gk14
+              gk13 : (x ∙ u) ∙ gk1n  ≈ a
+              gk13 = begin
+                 x ∙ u ∙ gk1n  ≈⟨ grefl ⟩ 
+                 x ∙ u ∙ naN gk14  ≈⟨ anaN=x gk14 ⟩ 
+                 a ∙ v ⁻¹ ∙ v  ≈⟨ solve monoid ⟩ 
+                 a ∙ (v ⁻¹ ∙ v)  ≈⟨ cdr ( proj₁ inverse _)  ⟩ 
+                 a ∙ ε  ≈⟨ solve monoid  ⟩ 
+                 a ∎
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H )