# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674687324 -32400
# Node ID 33d248c9081ec8b71da13398ca1b58afeb89ee01
# Parent  691b2ee844efbeb900498927795206a330291c74
...

diff -r 691b2ee844ef -r 33d248c9081e src/Fundamental.agda
--- a/src/Fundamental.agda	Thu Jan 26 01:16:38 2023 +0900
+++ b/src/Fundamental.agda	Thu Jan 26 07:55:24 2023 +0900
@@ -58,6 +58,9 @@
        ⟦_⟧ : Group.Carrier A → Group.Carrier A 
        normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
        comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b 
+       -- this is not explict stared in the standard group theory
+       factor : (a b : Carrier) → Carrier
+       is-factor : (a b : Carrier) →  b ∙ ⟦ factor a b ⟧ ≈ a
 
 -- Set of a ∙ ∃ n ∈ N
 --
@@ -70,10 +73,9 @@
 
 open import Tactic.MonoidSolver using (solve; solve-macro)
 
-
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
-    Carrier  = (x : Group.Carrier A  ) → aN N x
+    Carrier  = (x : Group.Carrier A) → aN N x
     ; _≈_      = _=n=_
     ; _∙_      = qadd 
     ; ε        = qid
@@ -150,9 +152,7 @@
     open EqReasoning (Algebra.Group.setoid G)
 
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g x = record { a = g  ; n = g ⁻¹ ∙ x ; aN=x = ? } where
-        gk00 :  g ∙ ⟦ ? ⟧ ≈ x
-        gk00 = ?
+    φ g x = record { a = g  ; n = factor x g ; aN=x = is-factor x g  } 
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ 
     φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
@@ -164,17 +164,32 @@
            φ-cong = ?
 
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f = ⟦ n (f ε) ⟧ 
+    inv-φ f = a (f ε) ∙ ⟦ n (f ε) ⟧ where
+         afn = (a (f (a (f ε) ∙ ⟦ n (f ε) ⟧))) ⁻¹
 
     cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
     cong-i = ?
 
+    factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧
+    factor=nf f {y} with f y
+    ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin
+       ⟦ factor y z ⟧ ≈⟨ ? ⟩ 
+       z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ 
+       z ⁻¹ ∙ y  ≈⟨ ? ⟩ 
+       z ⁻¹ ∙ fa ∙ ⟦ fn ⟧   ≈⟨ ? ⟩ 
+       ⟦ fn ⟧ ∎ where
+          z = fa ⁻¹
+
     is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
     is-inverse f {y} = begin
-       ⟦ n (φ (inv-φ f) y) ⟧  ≈⟨ ? ⟩
-       ⟦ n (φ (n (f ε)) y) ⟧  ≈⟨ ? ⟩
-       ⟦ ε ⟧  ≈⟨ ? ⟩
-       ⟦ n (f y) ⟧ ∎ 
+       ⟦ n (φ (inv-φ f) y) ⟧  ≈⟨ grefl G ⟩
+       ⟦ n (φ (a (f ε) ∙ ⟦ n (f ε) ⟧) y) ⟧  ≈⟨ grefl G ⟩
+       ⟦ factor y (a (f ε) ∙ ⟦ n (f ε) ⟧) ⟧  ≈⟨ grefl G ⟩
+       ⟦ factor y afn ⟧  ≈⟨ ? ⟩
+       ⟦ factor y afn' ⟧  ≈⟨ factor=nf f ⟩
+       ⟦ n (f y) ⟧ ∎ where
+           afn = a (f ε) ∙ ⟦ n (f ε) ⟧
+           afn' = (a (f y)) ⁻¹
 
     φ-surjective : Surjective φe 
     φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where