Mercurial > hg > Members > kono > Proof > category

changeset 1102:e50368495cf1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add gorup
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 24 Jan 2023 20:25:02 +0900
parents f485f725b2d3
children 57683a6e5674
files src/CCChom.agda src/cat-utility.agda src/group.agda src/pullback.agda
diffstat 4 files changed, 223 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCChom.agda	Thu Nov 03 11:01:18 2022 +0900
+++ b/src/CCChom.agda	Tue Jan 24 20:25:02 2023 +0900
@@ -246,10 +246,10 @@
 CCCtoAdj  A ccc b = record {
         U  = λ a → a <= b 
    ;    ε  = ε'
-   ;    _*'  = solution
+   ;    _*  = solution
    ;    iscoUniversalMapping = record {
            couniversalMapping = couniversalMapping
-         ; couniquness = couniquness
+         ; uniquness = uniquness
      }
   } where
    open CCC.CCC ccc
@@ -263,10 +263,10 @@
             {f : Hom A (FObj (F_b A ccc b) a) b₁} →
             A [ A [ ε' b₁ o FMap (F_b A ccc b) (solution f) ] ≈ f ]
    couniversalMapping {c} {a} {f} = IsCCC.e4a isc
-   couniquness :  {b = b₁ : Obj A} {a : Obj A}
+   uniquness :  {b = b₁ : Obj A} {a : Obj A}
             {f : Hom A (FObj (F_b A ccc b) a) b₁} {g : Hom A a (b₁ <= b)} →
             A [ A [ ε' b₁ o FMap (F_b A ccc b) g ] ≈ f ] → A [ solution f ≈ g ]
-   couniquness {c} {a} {f} {g} eq = begin
+   uniquness {c} {a} {f} {g} eq = begin
                  f *
              ≈↑⟨ *-cong eq ⟩
                   ( ε o FMap (F_b A ccc b) g ) *
--- a/src/cat-utility.agda	Thu Nov 03 11:01:18 2022 +0900
+++ b/src/cat-utility.agda	Tue Jan 24 20:25:02 2023 +0900
@@ -53,23 +53,23 @@
                          ( F : Functor A B )
                          ( U : Obj B → Obj A )
                          ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b )
-                         ( _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b ) )
+                         ( _* : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b ) )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
            field
                couniversalMapping :   {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } →
-                             B [ B [ ε b o FMap F ( f *' )  ]  ≈ f ]
-               couniquness :   {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g :  Hom A a (U b) } →
-                             B [ B [ ε b o FMap F g ]  ≈ f ] → A [ f *' ≈ g ]
+                             B [ B [ ε b o FMap F ( f * )  ]  ≈ f ]
+               uniquness :   {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g :  Hom A a (U b) } →
+                             B [ B [ ε b o FMap F g ]  ≈ f ] → A [ f * ≈ g ]
 
         record coUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( F : Functor A B )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-            infixr 11 _*'
+            infixr 11 _*
             field
                U : Obj B → Obj A 
                ε : (b : Obj B) → Hom B ( FObj F (U b) ) b 
-               _*' :  { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b )
-               iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'
+               _* :  { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b )
+               iscoUniversalMapping : coIsUniversalMapping A B F U ε _*
 
         open NTrans
         open import Category.Cat
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/group.agda	Tue Jan 24 20:25:02 2023 +0900
@@ -0,0 +1,204 @@
+-- Free Group and it's Universal Mapping 
+---- using Sets and forgetful functor
+
+-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+module group { c c₁ c₂ ℓ : Level }   where
+
+open import Category.Sets
+open import Category.Cat
+open import HomReasoning
+open import cat-utility
+open import Relation.Binary.Structures
+open import universal-mapping 
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+-- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeGroup.agda
+
+open import Algebra
+open import Algebra.Definitions -- using (Op₁; Op₂)
+open import Algebra.Core
+open import Algebra.Structures
+open import Data.Product
+
+record ≡-Group : Set (suc c) where
+  infixr 9 _∙_
+  field
+    Carrier  : Set c
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    _⁻¹      : Carrier → Carrier
+    isGroup : IsGroup _≡_ _∙_ ε _⁻¹
+
+_<_∙_> :  (m : ≡-Group)  →    ≡-Group.Carrier m →  ≡-Group.Carrier m →  ≡-Group.Carrier m
+m < x ∙ y > =  ≡-Group._∙_ m x y
+
+infixr 9 _<_∙_>
+
+record Homomorph ( a b : ≡-Group )  : Set c where
+  field
+      morph :  ≡-Group.Carrier a →  ≡-Group.Carrier b  
+      identity     :  morph (≡-Group.ε a)   ≡  ≡-Group.ε b
+      inverse      :  ∀{x} → morph ( ≡-Group._⁻¹ a x)  ≡   ≡-Group._⁻¹ b (morph  x) 
+      homo :  ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph  x  ∙ morph  y >
+
+open Homomorph
+
+_*_ : { a b c : ≡-Group } → Homomorph b c → Homomorph a b → Homomorph a c
+_*_ {a} {b} {c} f g =  record {
+      morph = λ x →  morph  f ( morph g x ) ;
+      identity  = identity1 ;
+      inverse  = inverse1 ;
+      homo  = homo1 
+   } where
+      open  ≡-Group 
+      identity1 : morph f ( morph g (ε a) )  ≡  ε c
+      identity1 = let open ≡-Reasoning in begin
+         morph f (morph g (ε a)) ≡⟨  cong (morph f ) ( identity g )  ⟩
+         morph f (ε b) ≡⟨  identity f  ⟩
+         ε c ∎ 
+      homo1 :  ∀{x y} → morph f ( morph g ( a < x ∙  y > )) ≡ ( c <   (morph f (morph  g x )) ∙(morph f (morph  g y) ) > )
+      homo1 {x} {y} = let open ≡-Reasoning in begin
+         morph f (morph g (a < x ∙ y >)) ≡⟨  cong (morph f ) ( homo g) ⟩
+         morph f (b < morph g x ∙ morph g y >) ≡⟨  homo f ⟩
+         c < morph f (morph g x) ∙ morph f (morph g y) > ∎ 
+      inverse1 : {x : Carrier a} → morph f (morph g ((a ⁻¹) x)) ≡ (c ⁻¹) (morph f (morph g x))
+      inverse1 {x} = begin 
+         morph f (morph g (_⁻¹ a x))  ≡⟨  cong (morph f) (inverse g) ⟩
+         morph f (_⁻¹ b (morph g x))   ≡⟨ inverse f ⟩
+         _⁻¹ c (morph f (morph g x)) ∎ where  open ≡-Reasoning 
+
+
+M-id : { a : ≡-Group } → Homomorph a a 
+M-id = record { morph = λ x → x  ; identity = refl ; homo = refl ; inverse = refl }
+
+_==_ : { a b : ≡-Group } → Homomorph a b → Homomorph a b → Set c 
+_==_  f g =  morph f ≡ morph g
+
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+-- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+-- postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 
+
+isGroups : IsCategory ≡-Group Homomorph _==_  _*_  (M-id)
+isGroups  = record  { isEquivalence =  isEquivalence1 
+                    ; identityL =  refl
+                    ; identityR =  refl
+                    ; associative = refl
+                    ; o-resp-≈ =    λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
+                    }
+     where
+        isEquivalence1 : { a b : ≡-Group } → IsEquivalence {_} {_} {Homomorph a b}  _==_ 
+        isEquivalence1  =      -- this is the same function as A's equivalence but has different types
+           record { refl  = refl
+             ; sym   = sym
+             ; trans = trans
+             } 
+        o-resp-≈ :  {a b c :  ≡-Group } {f g : Homomorph a b } → {h i : Homomorph b c }  → 
+                          f ==  g → h ==  i → (h * f) ==  (i * g)
+        o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i =  let open ≡-Reasoning in begin
+             morph ( h * f )
+         ≡⟨ cong ( λ  g → ( ( λ (x : ≡-Group.Carrier a ) →  g x ) )) (extensionality (Sets ) {≡-Group.Carrier a} lemma11) ⟩
+             morph ( i * g )
+         ∎  where
+            lemma11 : (x : ≡-Group.Carrier a) → morph (h * f) x ≡ morph (i * g) x
+            lemma11 x =   let open ≡-Reasoning in begin
+                  morph ( h * f ) x ≡⟨⟩
+                  morph h ( ( morph f ) x ) ≡⟨   cong ( λ y -> morph h ( y x ) )  f==g ⟩
+                  morph h ( morph g x ) ≡⟨   cong ( λ y -> y ( morph g  x ) )  h==i ⟩
+                  morph i ( morph g x ) ≡⟨⟩
+                  morph ( i * g ) x ∎
+
+Groups : Category _ _ _
+Groups  =
+  record { Obj =  ≡-Group 
+         ; Hom = Homomorph
+         ; _o_ = _*_  
+         ; _≈_ = _==_
+         ; Id  =  M-id
+         ; isCategory = isGroups 
+           }
+
+record NormalGroup (A : Obj Groups )  : Set (suc c) where
+   field 
+       normal :  Hom Groups A A 
+       comm : {a b :  ≡-Group.Carrier A} → A < b ∙ morph normal a > ≡ A < morph normal a ∙ b >
+
+-- Set of a ∙ ∃ n ∈ N
+--
+record aN {A : Obj Groups }  (N : NormalGroup A ) (x : ≡-Group.Carrier A  ) : Set c where 
+    field 
+        a n : ≡-Group.Carrier A 
+        x=aN : A < a ∙ morph (NormalGroup.normal N) n > ≡ x
+
+open import Tactic.MonoidSolver using (solve; solve-macro)
+
+qadd : (A : Obj Groups ) (N  : NormalGroup A ) → (f g : (x : ≡-Group.Carrier A  )  → aN N x ) → (x : ≡-Group.Carrier A  )  → aN N x
+qadd A N f g x = qadd1 where
+       open ≡-Group A
+       open aN
+       open NormalGroup 
+       qadd1 : aN N x
+       qadd1 = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; x=aN = q00 } where
+          m = morph (normal N)
+          q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ m (n (f x) ∙ n (g x))  ≡ x
+          q00 = begin
+             (x ⁻¹ ∙ (a (f x) ∙ a (g x))) ∙ m (n (f x) ∙ n (g x))  ≡⟨ ? ⟩ 
+             (a (f x) ∙ a (g x) ) ∙ m (n (f x) ∙ n (g x)) ∙ x ⁻¹ ≡⟨ cong ? (homo (normal N))  ⟩
+             (a (f x) ∙ a (g x) ) ∙ (m (n (f x)) ∙ m (n (g x))) ∙ x ⁻¹  ≡⟨ solve mono  ⟩
+             (a (f x) ∙ ((a (g x)  ∙ m (n (f x))) ∙ m (n (g x)))) ∙ x ⁻¹ ≡⟨ cong (λ k → ? ) (comm N) ⟩
+             (a (f x) ∙ ((m (n (f x))  ∙ a (g x)) ∙ m (n (g x)))) ∙ x ⁻¹ ≡⟨ solve mono ⟩
+             (a (f x) ∙ m (n (f x)) ) ∙ ((a (g x) ∙ m (n (g x))) ∙ x ⁻¹)  ≡⟨ cong (λ k → ? ) ?   ⟩
+             (a (f x) ∙ m (n (f x)) ) ∙ (x ∙ x ⁻¹)  ≡⟨ ?  ⟩
+             (a (f x) ∙ m (n (f x)) ) ∙ ε  ≡⟨ ?  ⟩
+             (a (f x) ∙ m (n (f x)) )  ≡⟨ x=aN (f x)  ⟩
+             x ∎ where 
+                open ≡-Reasoning
+                open IsGroup isGroup
+                mono : Monoid _ _
+                mono = record {isMonoid = isMonoid }
+
+_/_ : (A : Obj Groups ) (N  : NormalGroup A ) → ≡-Group 
+_/_ A N  = record {
+    Carrier  = (x : ≡-Group.Carrier A  ) → aN N x
+    ; _∙_      = qadd A N 
+    ; ε        = λ x → record { a = x  ; n = ε  ; x=aN = ?  }
+    ; _⁻¹      = λ f x → record { a = x ∙ (morph (normal N) (n (f x))) ⁻¹  ; n = n (f x)  ; x=aN = ?  }
+    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = record {refl = refl ; trans = trans ; sym = sym }
+       ; ∙-cong = ? }
+       ; assoc = ? }
+       ; identity = ( (λ q → ? ) , (λ q → ? ))  }
+       ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
+       ; ⁻¹-cong   = λ i=j → ?
+      }
+   } where
+       open ≡-Group A
+       open aN
+       open NormalGroup 
+
+φ : (G : Obj Groups ) (K  : NormalGroup G ) → Homomorph G (G / K )
+φ = ?
+
+GC : (G : Obj Groups ) → Category c c (suc c)
+GC G = ?
+
+U : (G H : Obj Groups ) → (f : Homomorph G H ) →  Functor (GC G) (GC H)
+U = ?
+
+
+fundamentalTheorem : (G H : Obj Groups ) → (K : NormalGroup G) → (f : Homomorph G H ) → UniversalMapping (GC G) (GC (G / K)) (U G H f )
+fundamentalTheorem G H K f = record { F = morph (φ G K)  ; η = eta ; _* = ? ; isUniversalMapping 
+       = record { universalMapping = λ {a} {b} {g} → is-solution a b g ; uniquness = ? }}  where
+     eta :  (a : Obj (GC G)) → Hom (GC G) a (Functor.FObj (U G H f) ( (morph (φ G K) a)) )
+     eta = ?
+     solution : {a : Obj (GC G)} {b : Obj (GC (G / K))} → Hom (GC G) a (Functor.FObj (U G H f) b) → Hom (GC (G / K)) (morph (φ G K) a) b
+     solution = ?
+     is-solution :  (a : Obj (GC G)) (b : Obj (GC (G / K)))
+            (g : Hom (GC G) a (Functor.FObj (U G H f) b)) →
+            (GC G) [ (GC G) [ Functor.FMap (U G H f) (solution {a} {b} g) o eta a ] ≈ g ]
+     is-solution = ?
+   
+
+
--- a/src/pullback.agda	Thu Nov 03 11:01:18 2022 +0900
+++ b/src/pullback.agda	Tue Jan 24 20:25:02 2023 +0900
@@ -239,9 +239,9 @@
 limit2couniv lim  = record {  
        U = λ b → a0 ( lim b) ;
        ε = λ b → t0 (lim b) ;
-       _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
+       _* = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
        iscoUniversalMapping = record { couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
-           couniquness = couniquness2
+           uniquness = uniquness2
        }
   } where
    couniversalMapping1 :  {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
@@ -253,10 +253,10 @@
         ≈⟨ t0f=t (isLimit (lim b)) ⟩
             TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
         ∎
-   couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (a0 (lim b ))} →
+   uniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (a0 (lim b ))} →
         ( ∀ { i : Obj I } → A [ A [ TMap (t0 (lim b )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] )
          → A [ limit (isLimit (lim b )) a f ≈ g ]
-   couniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
+   uniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
             limit (isLimit (lim b )) a f
         ≈⟨ limit-uniqueness (isLimit ( lim b )) lim-g=f ⟩
             g
@@ -279,21 +279,21 @@
      ε : ( b : Obj (A ^ I ) ) → NTrans I A (FObj (KI I) (U b)) b 
      ε b = coUniversalMapping.ε univ b
      limit1 :  (a : Obj A) → NTrans I A (FObj (KI I) a) Γ → Hom A a (U Γ)
-     limit1 a t = coUniversalMapping._*' univ {_} {a} t
+     limit1 a t = coUniversalMapping._* univ {_} {a} t
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K I A a) Γ}  {i : Obj I} →
                 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
             TMap (ε Γ) i o limit1 a t
         ≈⟨⟩
-            TMap (ε Γ) i o coUniversalMapping._*' univ t
+            TMap (ε Γ) i o coUniversalMapping._* univ t
         ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {a} {t} ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a (U Γ)}
          → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
      limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
-            coUniversalMapping._*' univ t
-        ≈⟨  ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
+            coUniversalMapping._* univ t
+        ≈⟨  ( coIsUniversalMapping.uniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
             f
         ∎