# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674546039 -32400
# Node ID c209aebeab2a5723fee3e7634e84d5c3fb3d4448
# Parent  0081e1ed5ead22d9f05c134747b5195cb1a2fc05
Fundamental again

diff -r 0081e1ed5ead -r c209aebeab2a src/Fundamental.agda
--- a/src/Fundamental.agda	Tue May 31 18:45:43 2022 +0900
+++ b/src/Fundamental.agda	Tue Jan 24 16:40:39 2023 +0900
@@ -7,11 +7,16 @@
 open import Algebra
 open import Algebra.Structures
 open import Algebra.Definitions
+open import Algebra.Core
+open import Algebra.Bundles
+
 open import Data.Product
 open import Relation.Binary.PropositionalEquality 
+open import Gutil0
+import Function.Definitions as FunctionDefinitions
+
+import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Algebra.Morphism.Structures 
-open GroupMorphisms
-open import Gutil0
 
 open import Tactic.MonoidSolver using (solve; solve-macro)
 
@@ -32,96 +37,92 @@
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-open HomoMorphism
+_<_∙_> :  (m : Group c l )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
+m < x ∙ y > =  Group._∙_ m x y
+
+infixr 9 _<_∙_>
 
 --
 --  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
 --
 
-record GSet (G : Group c l) : Set (Level.suc ( c  Level.⊔  l) ) where
-    field
-       def : ( x : Group.Carrier G ) → Set ( c  Level.⊔ l )
 
-open GSet
-
-record _==_ { G :  Group c l } (x y : GSet G ) : Set ( c  Level.⊔  (Level.suc l )) where
-    open Group G
-    field
-       eq→ : {g : Carrier } → def x g → def y g
-       eq← : {g : Carrier } → def y g → def x g
-
-open NormalSubGroup  -- G has at least an element other than ε
-
-record GCoset (G : Group c l)  (K : NormalSubGroup G) (base x : Group.Carrier G ) : Set ( c  Level.⊔  l)  where
-    open Group G
-    field
-       factor : Carrier
-       isCoset : x ≈ base ∙ sub K factor
-
-record Coset (G : Group c l)  (K : NormalSubGroup G) : Set ( c  Level.⊔  l)  where
-    open Group G
-    field
-       base : Carrier
-
-open Coset
-
-φset :   {G : Group c l} →  {K : NormalSubGroup G} → (g : Group.Carrier G ) → GSet G
-φset {G} {K} g = record { def = λ x → GCoset G K g x }
-
-φ :   {G : Group c l} →  {K : NormalSubGroup G} → (g : Group.Carrier G ) → Coset G K
-φ {G} {K} g = record { base = g }
-
---  Na ∙ Nb = Nab
-
-mul : {G : Group c l}  {K : NormalSubGroup G} → (x y :  Coset G K ) → Coset G K 
-mul {G} {K} x y  = record { base = base x ∙ base y } where open Group G
-
-inv : {G : Group c l}  {K : NormalSubGroup G} →  Coset G K   →  Coset G K 
-inv {G} {K} x = record { base  = (base x) ⁻¹ } where open Group G
-
--- import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
--- open HE
+open GroupMorphisms
 
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
--- G / K : Quotient
-_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) (c ⊔ Level.suc l)
-G / K = record {
-     Carrier        = Coset G K 
-     ; _≈_          = λ x y → φset {G} {K} (base x) == φset {G} {K} (base y)
-     ; _∙_          = λ x y → mul x y
-     ; ε            = record { base = ε }
-     ; _⁻¹          = λ x → inv x
-     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record { refl = {!!} ; sym = {!!} ; trans = {!!} } 
-       ; ∙-cong = λ {x y u v} → {!!} }
-       ; assoc = {!!} }
-       ; identity = {!!} }
-       ; inverse   = {!!}
-       ; ⁻¹-cong   = λ {x} {y} → {!!}
-      } 
-   } where 
-      open Group G hiding (refl ; sym ; trans )
-      open EqReasoning (Algebra.Group.setoid G)
-      open IsGroupHomomorphism (s-homo K )
+record NormalSubGroup (A : Group (c ⊔ l) l )  : Set (c ⊔ l)  where
+   open Group A
+   field  
+       ⟦_⟧ : Group.Carrier A → Group.Carrier A 
+       normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
+       comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b 
+
+-- Set of a ∙ ∃ n ∈ N
+--
+record aN {A : Group (c ⊔ l) l }  (N : NormalSubGroup A ) (x : Group.Carrier A  ) : Set (c ⊔ l) where 
+    open Group A
+    open NormalSubGroup N
+    field 
+        a n : Group.Carrier A 
+        aN=x :  a ∙ ⟦ n ⟧ ≈ x
+
+open import Tactic.MonoidSolver using (solve; solve-macro)
+
+_/_ : (A : Group (c ⊔ l) l ) (N  : NormalSubGroup A ) → Group (c ⊔ l) l
+_/_ A N  = record {
+    Carrier  = (x : Group.Carrier A  ) → aN N x
+    ; _≈_      = ?
+    ; _∙_      = _+_
+    ; ε        = λ 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 = ? }
+       ; ∙-cong = ? }
+       ; assoc = ? }
+       ; identity =  ? , (λ q → ? )  }
+       ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
+       ; ⁻¹-cong   = λ i=j → ?
+      }
+   } where
+       open Group A
+       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
+
 
 -- K ⊂ ker(f)
-K⊆ker : (G H : Group c 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 ( sub K x ) ≈ ε   where
+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
   open Group H
 
-record FundamentalHomomorphism (G H : Group c l)  
+record FundamentalHomomorphism (G H : Group (c ⊔ l) l)  
     (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
   open Group H
   field
-    h : Coset G K → Group.Carrier H
-    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
+    h : ? → Group.Carrier H
+    h-homo :  IsGroupHomomorphism (GR (G / ?) ) (GR H) h
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( ? x )
 
-FundamentalHomomorphismTheorm : (G H : Group c l)
+FundamentalHomomorphismTheorm : (G H : Group (c ⊔ l) l)
     (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
@@ -131,12 +132,12 @@
    ; unique = unique
   } where
     open Group H
-    h : Coset G K → Carrier   --  G / K → H
-    h r = f (base r)
+    h : ? G K → Carrier   --  G / K → H
+    h r = f ?
     _o_ = Group._∙_ G
-    h03 : (x y : Group.Carrier (G / K ) ) →  h ( mul x y ) ≈ h x ∙ h y
+    h03 : (x y : Group.Carrier (G / ? ) ) →  h ( ? x y ) ≈ h x ∙ h y
     h03 x y = {!!}
-    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
+    h-homo :  IsGroupHomomorphism (GR (G / ? ) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
@@ -144,10 +145,10 @@
            ; homo = h03 }
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( ? x )
     unique x = begin
          f x ≈⟨ grefl H ⟩
-         h ( φ x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
+         h ( ? x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
 
 
 
diff -r 0081e1ed5ead -r c209aebeab2a src/Gutil.agda
--- a/src/Gutil.agda	Tue May 31 18:45:43 2022 +0900
+++ b/src/Gutil.agda	Tue Jan 24 16:40:39 2023 +0900
@@ -128,3 +128,17 @@
      (f ∙ g) ⁻¹
      ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+open import Tactic.MonoidSolver using (solve; solve-macro)
+
+lemma7 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
+lemma7 f g = begin
+     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ solve monoid ⟩
+     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
+     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ solve monoid ⟩
+     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
+     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ solve monoid ⟩
+     (f ∙ g) ⁻¹
+     ∎ where open EqReasoning (Algebra.Group.setoid G)
+
diff -r 0081e1ed5ead -r c209aebeab2a src/Gutil0.agda
--- a/src/Gutil0.agda	Tue May 31 18:45:43 2022 +0900
+++ b/src/Gutil0.agda	Tue Jan 24 16:40:39 2023 +0900
@@ -54,27 +54,27 @@
 gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z
 gtrans G = IsGroup.trans ( Group.isGroup G )
 
-record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     sub : Carrier → Carrier 
-     s-homo  : IsGroupHomomorphism (GR G) (GR G) sub
-     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
-     -- it has at least one element other than ε 
-     -- anElement : Carrier
-     -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) )
+-- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c  Level.⊔  l ) where
+--  open Group G
+--  field
+--     sub : Carrier → Carrier 
+--     s-homo  : IsGroupHomomorphism (GR G) (GR G) sub
+--     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
+--     -- it has at least one element other than ε 
+--     -- anElement : Carrier
+--     -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) )
 
 -- open import Relation.Binary.Morphism.Structures
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-record HomoMorphism {c l : Level } (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
-     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
-     f-ε : f ( ε ) ≈ ε
-     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
+-- record HomoMorphism {c l : Level } (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
+--  open Group G
+--  field
+--     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
+--     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
+--     f-ε : f ( ε ) ≈ ε
+--     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
 
 -- HM : {c l : Level } → (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
 --   → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f