# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674976089 -32400
# Node ID f257ab4afa516da5867b4854bd39c4a980f8c666
# Parent  515de7624a0c1cb523b00656d7e300213ef724e0
...

diff -r 515de7624a0c -r f257ab4afa51 src/FundamentalHomorphism.agda
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 13:09:54 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 16:08:09 2023 +0900
@@ -55,6 +55,8 @@
 -- import Axiom.Extensionality.Propositional
 -- postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
+open import Data.Empty
+open import Relation.Nullary
 
 record NormalSubGroup (A : Group c c )  : Set c  where
    open Group A
@@ -62,7 +64,7 @@
        ⟦_⟧ : Group.Carrier A → Group.Carrier A
        normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
        comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b
-       --
+       -- because of ¬ ¬ Factor
        factor : (a b : Carrier) → Carrier
        is-factor : (a b : Carrier) →  b ∙ ⟦ factor a b ⟧ ≈ a
 
@@ -81,6 +83,49 @@
         n : Carrier 
         is-an : (x : Carrier) → an N n x
 
+record Factor (A : Group c c ) (N : NormalSubGroup A) (a b : Group.Carrier A )  : Set c  where
+   open Group A
+   open NormalSubGroup N
+   open IsGroupHomomorphism normal
+   field
+       factor : Carrier
+       is-factor : b ∙ ⟦ factor ⟧ ≈ a
+
+¬¬Factor : (A : Group c c ) (N : NormalSubGroup A) → ¬ ¬ ( (a b : Group.Carrier A )  →  Factor A N a b )
+¬¬Factor A N neg = ⊥-elim ( fa ( λ y → record { n = y ; is-an = λ x → record { a = x ∙ ⟦ y ⟧ ⁻¹ ; aN=x = f03 } }  ))  where
+   open Group A
+   open NormalSubGroup N
+   open IsGroupHomomorphism normal
+   open EqReasoning (Algebra.Group.setoid A)
+   open Gutil A
+   open aN
+   f03 : {x y : Carrier } → x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈ x
+   f03 {x} {y} = begin
+      x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈⟨ ? ⟩ 
+      x ∙ ( ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧)  ≈⟨ ? ⟩ 
+      x ∎
+   fa : ¬ ( (x : Carrier) →  aN N ) 
+   fa f = neg ( λ a b →  record { factor = n (f ( a ∙ b ⁻¹)) ; is-factor = fa01 a b }  ) where
+        fa01 : (a b : Carrier ) →  b ∙  ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈ a 
+        fa01 a b = begin
+           b ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧  ≈⟨ ? ⟩ 
+           b ∙ (ε ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ) ≈⟨ ? ⟩ 
+           b ∙ (( f02  ⁻¹ ∙  f02 ) ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ) ≈⟨ ? ⟩ 
+           b ∙ ( f02  ⁻¹ ∙ ( f02  ∙  ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ))  ≈⟨ cdr ( cdr ( an.aN=x (is-an  (f ( a ∙ b ⁻¹)) (f05 ∙ a)  )))  ⟩ 
+           b ∙ (f02 ⁻¹ ∙ ( f05  ∙ a))  ≈⟨ ? ⟩ 
+           b ∙ ( (f02 ⁻¹ ∙ f02 ) ∙ b ⁻¹)  ∙ a  ≈⟨ ? ⟩ 
+           b ∙ ( ε ∙ b ⁻¹)  ∙ a  ≈⟨ ? ⟩ 
+           b ∙ ( b ⁻¹ ∙ a )   ≈⟨ ? ⟩ 
+           (b ∙  b ⁻¹ ) ∙ a    ≈⟨ ? ⟩ 
+           ε ∙ a    ≈⟨ ? ⟩ 
+           a  ∎  where
+               f05 : Carrier
+               f05 = a ∙ b ⁻¹
+               f02 : Carrier
+               f02 = an.a (is-an (f (a ∙ b ⁻¹)) (f05 ∙ a))
+               f04 : f02 ∙ b ⁻¹ ≈ f05
+               f04 = ?
+
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
     Carrier  = aN N