# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1693984244 -32400
# Node ID 3ca1d0e379d05347e1d458863249f5d792d5ff71
# Parent  e2c48fac6215a20c795cd0e892d54e01480da300
quontient group done

diff -r e2c48fac6215 -r 3ca1d0e379d0 src/homomorphism.agda
--- a/src/homomorphism.agda	Wed Sep 06 11:21:39 2023 +0900
+++ b/src/homomorphism.agda	Wed Sep 06 16:10:44 2023 +0900
@@ -74,7 +74,7 @@
     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 n1 _ an03 Pε where
+                  , an n2 _ an03 Pε where
         an04 : x ∙ y ∙ n  ≈ a 
         an04 = eqa
         -- n ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)
@@ -129,6 +129,16 @@
     aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt }   
     -- this may wrong 
     -- aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x)  →  naN ia ≈ naN ib
+    ayxi : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → IsaN N y (x ∙ n)
+    ayxi {x} {y} x=y {n} pn = eq→ x=y (an n _ grefl pn)
+    ayxn : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → Carrier
+    ayxn {x} {y} x=y {n} pn = naN (ayxi x=y pn)
+    Payxn : {x y : Carrier} → (x=y : aNeq N x y) → {n : Carrier} → (pn : P n) → P (ayxn x=y pn)
+    Payxn {x} {y} x=y {n} pn with ayxi x=y pn
+    ... | an n₁ .((A Group.∙ x) n) x₁ pn₁ = pn₁
+    anxn=yn : {x y n : Carrier } → (x=y : aNeq N x y) → (pn : P n) → x ∙ n ≈ y ∙ (ayxn x=y pn)
+    anxn=yn {x} {y} {n} x=y pn with ayxi x=y pn
+    ... | an n₁ .((A Group.∙ x) n) eq1 pn₁ = gsym eq1
 
 _/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
@@ -163,9 +173,10 @@
        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
+       gk00 {x} {y} {u} {v} x=y u=v = record { eq→ = gk01 x=y u=v ; eq← =  gk01 (nsym x=y) (nsym u=v) } where
+           -- xN ≈ yN → uN ≈ vN → xuN ≈ xN⁻¹NuN  ≈ yN⁻¹NvN  ≈ yvN
+           gk01 : {a x y u v : Carrier} → aNeq N x y → aNeq N u v  → IsaN N (x ∙ u) a → IsaN N (y ∙ v) a
+           gk01 {a} {x} {y} {u} {v} x=y u=v (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
@@ -182,24 +193,6 @@
                  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 ∎
        gkassoc : (x y z : Carrier ) → aNeq N ((x ∙ y ) ∙ z) (x ∙ (y ∙ z))
        gkassoc x y z = record { eq→ = gk04 ; eq← =  gk06 }  where
           gk04 : {a : Carrier } →  IsaN N (x ∙ y ∙ z) a → IsaN N (x ∙ (y ∙ z)) a
@@ -217,28 +210,23 @@
                  x ∙ (y ∙ z) ∙ n  ≈⟨ eq ⟩
                  a ∎
        gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) 
-       gkcong⁻¹ {x} {y} x=y  = record { eq→ = gk07 ; eq← =  gk08 }  where
+       gkcong⁻¹ {x} {y} x=y  = record { eq→ = gk07 x=y ; eq← =  gk07 (nsym x=y) }  where
           --  a⁻¹N     ≈ (Na)⁻¹          ≈ (aN)⁻¹        ≈ (bN)⁻¹        ≈ (Nb)⁻¹         ≈ b⁻¹N
           --  a ⁻¹ ∙ n ≈ ( n ⁻¹ ∙ a ) ⁻¹ ≈ ( a ∙ n₁ ) ⁻¹ ≈ ( b ∙ n₂ ) ⁻¹ ≈ ( n₃  ∙ b ) ⁻¹ ≈ b ⁻¹ ∙ n₃
-          gk07 : {a : Carrier } →  IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a
-          gk07 {a} (an n _ eq pn) = an ? _ ? ? where
-              gk01 : y ⁻¹ ∙ ?  ≈ a
+          gk07 : {a x y : Carrier } → (x=y : aNeq N x y) →  IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a
+          gk07 {a} {x} {y} x=y (an n _ eq pn) = an ((conj (ayxn x=y pj) y )⁻¹)  _ gk01 (P⁻¹ _ (Pconj _ _ (Payxn x=y pj ) ) ) where
+              pj : P (conj (n ⁻¹) (x ⁻¹)) 
+              pj = Pcomm (P⁻¹ _ pn) 
+              gk01 : y ⁻¹ ∙  (conj (ayxn x=y pj) y ) ⁻¹  ≈ a
               gk01 = begin
-                 y ⁻¹ ∙ ?  ≈⟨ ? ⟩
-                 (?  ∙ y ) ⁻¹  ≈⟨ ?  ⟩
-                 (y ∙ ?  ) ⁻¹  ≈⟨ ?  ⟩
+                 y ⁻¹ ∙ (conj (ayxn x=y pj) _ ) ⁻¹   ≈⟨ lemma5 _ _  ⟩
+                 ( conj (ayxn x=y pj) _ ∙ y ) ⁻¹  ≈⟨  ⁻¹-cong (gsym aN=Na)  ⟩
+                 (y ∙ ayxn x=y pj ) ⁻¹  ≈⟨ gsym ( ⁻¹-cong ( anxn=yn x=y pj ))  ⟩
                  (x ∙ conj (n ⁻¹) (x ⁻¹) ) ⁻¹  ≈⟨  ⁻¹-cong (gsym Na=aN )  ⟩
-                 (n ⁻¹ ∙ x ) ⁻¹  ≈⟨ ?  ⟩
-                 x ⁻¹ ∙ (n ⁻¹) ⁻¹   ≈⟨ ? ⟩
+                 (n ⁻¹ ∙ x ) ⁻¹  ≈⟨ gsym (lemma5 _ _  ) ⟩
+                 x ⁻¹ ∙ (n ⁻¹) ⁻¹   ≈⟨ cdr f⁻¹⁻¹≈f ⟩
                  x ⁻¹ ∙ n  ≈⟨ eq ⟩
                  a ∎
-          gk08 : {a : Carrier } →  IsaN N (y ⁻¹) a → IsaN N (x ⁻¹) a
-          gk08 {a} (an n _ eq pn) = an n _ gk05 pn where
-              gk05 :  x ⁻¹ ∙ n  ≈ a
-              gk05 = begin
-                 x ⁻¹ ∙ n  ≈⟨ ? ⟩
-                 y ⁻¹ ∙ n  ≈⟨ eq ⟩
-                 a ∎
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) 
@@ -255,33 +243,34 @@
     open NormalSubGroup K
     open EqReasoning (Algebra.Group.setoid G)
     open Gutil G
+    open AN G K
 
-    gkε : ?
-    gkε = ? -- record { a = ε ; n = ε ; pn = Pε }
+    gkε : Group.Carrier (G / K)
+    gkε = Group.ε (G / K) 
 
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g = ?
+    φ g = g
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
-    φ-homo = record {⁻¹-homo = ? ; isMonoidHomomorphism = record { ε-homo = ?
-           ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
-       record { cong = ? } }}} where
+    φ-homo = record {⁻¹-homo = λ x → aneq grefl ; isMonoidHomomorphism = record { ε-homo = aneq grefl
+           ; isMagmaHomomorphism = record { homo = λ x y → aneq grefl ; isRelHomomorphism =
+       record { cong = λ eq → aneq eq } }}} where
 
 
     φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
     φe = record { _⟨$⟩_ = φ ; cong = gk40 }  where
           gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j >
-          gk40 {i} {j} i=j = ?
+          gk40 {i} {j} i=j = aneq i=j
 
     inv-φ : Group.Carrier (G / K ) → Carrier 
-    inv-φ = ? -- record { a = a ; n = n ; pn = pn } = a ∙ n 
+    inv-φ x = ?
 
     φ-surjective : Surjective φe
-    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → ? }
-          ; right-inverse-of = ? } where
-       gk50 :  (f g : Group.Carrier (G / K)) → ? ≈ ? → inv-φ f ≈ inv-φ g
-       gk50 = ?
-       gk60 : (x : Group.Carrier (G / K )) → inv-φ x ∙ ε ≈ ?
+    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → gk50 f g }
+          ; right-inverse-of = gk60 } where
+       gk50 :  (f g : Group.Carrier (G / K)) → (G / K) < f ≈ g > → inv-φ f ≈ inv-φ g
+       gk50 f g f=g = ?
+       gk60 : (x : Group.Carrier (G / K )) → aNeq K (φ (inv-φ x)) x
        gk60 = ?
 
     gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >