# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674555338 -32400
# Node ID ce372f6347d6ff76a63ad1675227c19e2325980c
# Parent  c209aebeab2a5723fee3e7634e84d5c3fb3d4448
Foundamental definition done

diff -r c209aebeab2a -r ce372f6347d6 src/Fundamental.agda
--- a/src/Fundamental.agda	Tue Jan 24 16:40:39 2023 +0900
+++ b/src/Fundamental.agda	Tue Jan 24 19:15:38 2023 +0900
@@ -2,7 +2,7 @@
 --
 
 open import Level hiding ( suc ; zero )
-module Fundamental (c l : Level) where
+module Fundamental (c : Level) where
 
 open import Algebra
 open import Algebra.Structures
@@ -37,7 +37,7 @@
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-_<_∙_> :  (m : Group c l )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
+_<_∙_> :  (m : Group c c )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
 m < x ∙ y > =  Group._∙_ m x y
 
 infixr 9 _<_∙_>
@@ -52,7 +52,7 @@
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
-record NormalSubGroup (A : Group (c ⊔ l) l )  : Set (c ⊔ l)  where
+record NormalSubGroup (A : Group c c )  : Set c  where
    open Group A
    field  
        ⟦_⟧ : Group.Carrier A → Group.Carrier A 
@@ -61,7 +61,7 @@
 
 -- Set of a ∙ ∃ n ∈ N
 --
-record aN {A : Group (c ⊔ l) l }  (N : NormalSubGroup A ) (x : Group.Carrier A  ) : Set (c ⊔ l) where 
+record aN {A : Group c c }  (N : NormalSubGroup A ) (x : Group.Carrier A  ) : Set c where 
     open Group A
     open NormalSubGroup N
     field 
@@ -70,18 +70,37 @@
 
 open import Tactic.MonoidSolver using (solve; solve-macro)
 
-_/_ : (A : Group (c ⊔ l) l ) (N  : NormalSubGroup A ) → Group (c ⊔ l) l
+qadd : (A : Group c c ) (N  : NormalSubGroup A ) → (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
+qadd A N  f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
+       open Group A
+       open aN
+       open NormalSubGroup N
+       open IsGroupHomomorphism normal 
+       q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
+       q00 = begin 
+          ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
+          x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
+          x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) ))  ⟩
+          x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
+          x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl A) (aN=x (g x)  ) ⟩
+          x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A)  ⟩
+          (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A)  ⟩
+          ε ∙ x  ≈⟨ solve monoid  ⟩
+          x ∎ where 
+            open EqReasoning (Algebra.Group.setoid A)
+
+_/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
     Carrier  = (x : Group.Carrier A  ) → aN N x
-    ; _≈_      = ?
-    ; _∙_      = _+_
+    ; _≈_      = _=n=_
+    ; _∙_      = qadd A N
     ; ε        = λ x → record { a = x  ; n = ε  ; x=aN = ?  }
     ; _⁻¹      = λ f x → record { a = x ∙ ⟦ n (f x) ⟧  ⁻¹  ; n = n (f x)  ; x=aN = ?  }
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record {refl = ? ; trans = ? ; sym = ? }
+       isEquivalence = record {refl = grefl A  ; trans = ? ; sym = ? }
        ; ∙-cong = ? }
        ; assoc = ? }
-       ; identity =  ? , (λ q → ? )  }
+       ; identity =  idL , (λ q → ? )  }
        ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
        ; ⁻¹-cong   = λ i=j → ?
       }
@@ -90,54 +109,80 @@
        open aN
        open NormalSubGroup N
        open IsGroupHomomorphism normal 
-       _+_ : (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
-       _+_ f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
-          q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
-          q00 = begin 
-              ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
-              x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) ))  ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl A) (aN=x (g x)  ) ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A)  ⟩
-              (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A)  ⟩
-              ε ∙ x  ≈⟨ solve monoid  ⟩
-              x ∎ where 
-                open EqReasoning (Algebra.Group.setoid A)
-                -- open IsGroup isGroup
+       _=n=_ : (f g : (x : Group.Carrier A  )  → aN N x ) →  Set c
+       f =n= g = {x : Group.Carrier A  } → ⟦ n (f x) ⟧  ≈ ⟦ n (g x) ⟧  
+       qid : ( x : Carrier ) → aN N x
+       qid x = record { a = x  ; n = ε  ; x=aN = ?  }
+       idL : (f : (x  : Carrier )→  aN N x) → (qadd A N qid f ) =n= f 
+       idL f = ?
 
 
 -- K ⊂ ker(f)
-K⊆ker : (G H : Group (c ⊔ l) l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
-K⊆ker G H K f = (x : Group.Carrier G ) → f ( ? K x ) ≈ ε   where
+K⊆ker : (G H : Group c c)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
+K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε   where
   open Group H
+  open NormalSubGroup K
 
-record FundamentalHomomorphism (G H : Group (c ⊔ l) l)  
+φ : (G : Group c c)  (K : NormalSubGroup G) → Group.Carrier G → Group.Carrier (G / K )
+φ G K g = ?
+
+φ-homo : (G : Group c c)  (K : NormalSubGroup G) → IsGroupHomomorphism (GR G) (GR (G / K)) (φ G K)
+φ-homo = ?
+
+open import Function.Surjection
+open import Function.Equality
+
+φe : (G : Group c c)  (K : NormalSubGroup G) → (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
+φe G K = record { _⟨$⟩_ = φ G K   ; cong = φ-cong  }  where
+       open Group G
+       open aN
+       open NormalSubGroup K
+       open IsGroupHomomorphism normal 
+       φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ G K f x ) ⟧ ≈ ⟦ n (φ G K g x ) ⟧ 
+       φ-cong = ?
+
+φ-surjective : (G : Group c c)  (K : NormalSubGroup G) → Surjective (φe G K )
+φ-surjective G K = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where
+       open Group G
+       open aN
+       open NormalSubGroup K
+       open IsGroupHomomorphism normal 
+       inv-φ : Group.Carrier (G / K ) → Group.Carrier G
+       inv-φ = ?
+       cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
+       cong-i = ?
+       is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ G K (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
+       is-inverse = ?
+ 
+record FundamentalHomomorphism (G H : Group c c )
     (f : Group.Carrier G → Group.Carrier H ) 
     (homo : IsGroupHomomorphism (GR G) (GR H) f ) 
-    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔ ( Level.suc l) ) where
+    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set c where
   open Group H
   field
-    h : ? → Group.Carrier H
-    h-homo :  IsGroupHomomorphism (GR (G / ?) ) (GR H) h
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( ? x )
+    h : Group.Carrier (G / K ) → Group.Carrier H
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
+    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
+       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
 
-FundamentalHomomorphismTheorm : (G H : Group (c ⊔ l) l)
+FundamentalHomomorphismTheorm : (G H : Group c c)
     (f : Group.Carrier G → Group.Carrier H )
     (homo : IsGroupHomomorphism (GR G) (GR H) f )
     (K : NormalSubGroup G ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
 FundamentalHomomorphismTheorm G H f homo K kf = record {
      h = h
    ; h-homo = h-homo
+   ; is-solution = is-solution
    ; unique = unique
   } where
     open Group H
-    h : ? G K → Carrier   --  G / K → H
-    h r = f ?
+    h : Group.Carrier (G / K ) → Group.Carrier H
+    h r = ?
     _o_ = Group._∙_ G
-    h03 : (x y : Group.Carrier (G / ? ) ) →  h ( ? x y ) ≈ h x ∙ h y
+    h03 : (x y : Group.Carrier (G / K ) ) →  h ( qadd G K x y ) ≈ h x ∙ h y
     h03 x y = {!!}
-    h-homo :  IsGroupHomomorphism (GR (G / ? ) ) (GR H) h
+    h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
@@ -145,10 +190,13 @@
            ; homo = h03 }
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( ? x )
-    unique x = begin
+    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
+    is-solution x = begin
          f x ≈⟨ grefl H ⟩
-         h ( ? x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
+         h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
+       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
+    unique = ?