Mercurial > hg > Members > kono > Proof > category

changeset 1000:3ef1b472e9f9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
yoneda full and faithful
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Mar 2021 02:10:14 +0900
parents d89f2c8cf0f4
children 5861128f1e49
files src/CCCGraph.agda src/yoneda.agda
diffstat 2 files changed, 47 insertions(+), 139 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCGraph.agda	Mon Mar 08 08:25:30 2021 +0900
+++ b/src/CCCGraph.agda	Tue Mar 09 02:10:14 2021 +0900
@@ -218,14 +218,16 @@
 
 cat-graph-univ :  {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (CAT {c₁ } {c₁} {c₁}) forgetful.UC 
 cat-graph-univ {c₁}  = record {
-     F = {!!} ;
+     F = F ;
      η = {!!} ; 
      _* = {!!} ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
          uniquness = {!!}
       }
-  } 
+  }  where
+      F :  Obj (Grph {c₁} {c₁}) → Obj CAT
+      F g =  PL where open ccc-from-graph g
 
 open ccc-from-graph.Objs
 open ccc-from-graph.Arrow
@@ -297,7 +299,7 @@
             vm : (y : vertex a ) →  vertex (FObj UX (F a))
             vm y =  atom y
             em :  { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y)
-            em {x} {y} f = {!!} -- fmap a (iv (arrow f) (id _))
+            em {x} {y} f = iv (arrow f) (id _)  -- fmap a (iv (arrow f) (id _))
        cobj  :  {g : Obj (Grph {c₁} {c₁} ) } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
        cobj {g} {c} f (atom x) = vmap f x 
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
@@ -305,10 +307,12 @@
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
        c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs g} 
            → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       --- from x to b chain. but we forgot how we come here ...
-       c-map {g} {c} {atom x} {atom b} f y = {!!}
-       --- next three cases cannot be negerated
-       c-map {g} {c} {⊤} {atom b} f y = {!!}
+       c-map {g} {c} {atom x} {atom b} f y = {!!}  where
+            cmpa1 : ((y₁ : vertex g) → C g y₁ x ) → {!!}
+            cmpa1 = {!!}
+       c-map {g} {c} {⊤} {atom b} f y with y OneObj b
+       ... | id .b = {!!}
+       ... | next x t = (cat c) [ emap f x o c-map f {!!} ]
        c-map {g} {c} {a ∧ a₁} {atom b} f y = {!!}
        c-map {g} {c} {a <= a₁} {atom b} f y = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
--- a/src/yoneda.agda	Mon Mar 08 08:25:30 2021 +0900
+++ b/src/yoneda.agda	Tue Mar 09 02:10:14 2021 +0900
@@ -226,6 +226,9 @@
    isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj  a) F (F2Natmap  {a} {F})
    isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} } 
 
+--
+-- Obj Part : SetAop (Y - , F) ≅  F 
+--
 
 --  F(a) <- Nat(h_a,F)
 Nat2F :    {a : Obj A} → {F : Obj SetsAop  } →  Hom SetsAop  (y-obj  a) F  → FObj F a 
@@ -247,14 +250,10 @@
                 id1 Sets (FObj F a)
              ∎ )
 
--- open  import  Relation.Binary.PropositionalEquality
-
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
---     F :  op A → Sets
 --     ha : NTrans (op A) Sets (y-obj {a}) F
 --                FMap F  g  o TMap ha a ≈   TMap ha b  o FMap (y-obj {a}) g
-
 Nat2F→F2Nat :  {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop  (y-obj  a) F) 
      →  SetsAop  [ F2Nat  {a} {F} (Nat2F  {a} {F} ha) ≈ ha ]
 Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in begin
@@ -267,38 +266,36 @@
         TMap ha b
      ∎ 
 
--- SetAop (Y - , F) ≅ F is set of natural transformation
-
-Nat2F-ntrans : (a : Obj A) ( F : Obj SetsAop ) → NTrans (Category.op A) Sets (y-obj a) F
-Nat2F-ntrans a F = record { TMap = λ b f → TMap (F2Nat {a} {F} (Nat2F {!!}) ) b f ; isNTrans = record { commute = {!!} } }
-
-F2Nat-ntrans : (a : Obj A) ( F : Obj SetsAop ) → NTrans (Category.op A) Sets F (y-obj a) 
-F2Nat-ntrans a F = record { TMap = λ b f  → TMap (F2Nat {a} {y-obj a} (Nat2F {!!})) b {!!} ; isNTrans = record { commute = {!!} } }
-
 -- Yoneda's Lemma
 --    Yoneda Functor is full and faithfull
 --    that is FMapp Yoneda is injective and surjective
 
 --  λ b g → (A Category.o f₁) g
-YondaLemma1 :  {a a' : Obj A } {f : FObj (FObj YonedaFunctor  a) a' } 
+YonedaLemma1 :  {a a' : Obj A } {f : FObj (FObj YonedaFunctor  a) a' } 
      → SetsAop [ F2Nat  {a'} {FObj YonedaFunctor  a} f ≈ FMap YonedaFunctor  f ]
-YondaLemma1 {a} {a'} {f} = refl
+YonedaLemma1 {a} {a'} {f} = refl
+
+-- full (injective )
+YonedaIso0 :  {a a' : Obj A } {f : FObj (FObj YonedaFunctor  a) a' } 
+     → Nat2F ( FMap YonedaFunctor  f ) ≡ f
+YonedaIso0 {a} {a'} {f} = ≈-≡ A (≈-Reasoning.idR A)
+
+-- faithful (surjective)
+YonedaIso1 : {a a' : Obj A } →  (ha : Hom SetsAop  (y-obj  a) (y-obj a'))
+     →  SetsAop  [ FMap YonedaFunctor (Nat2F  {a} ha) ≈ ha ]
+YonedaIso1 {a} {a'} ha = Nat2F→F2Nat ha 
 
 domF : (y :  Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A
 domF y {x} z = x
 
---
--- f onto 
---
+YonedaLemma2 :  {a a' b : Obj A } (f : Hom A a  a' ) →  NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a')
+YonedaLemma2 f =  FMap YonedaFunctor  f
 
-YondaLemma2 :  {a a' b : Obj A } (f : Hom A a  a' ) →  NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a')
-YondaLemma2 f =  FMap YonedaFunctor  f
+YonedaLemma3 :  {a a' b : Obj A } (f : Hom A a  a' ) → (g : Hom A b a ) →  Hom A b a' -- f o g
+YonedaLemma3 {a} {a'} {b} f g = TMap  (FMap YonedaFunctor  f) b g
 
-YondaLemma3 :  {a a' b : Obj A } (f : Hom A a  a' ) → Hom A b a →  Hom A b a'
-YondaLemma3 {a} {a'} {b} f = TMap  (FMap YonedaFunctor  f) b 
-
--- YondaLemma4 :  {a a' b : Obj A }  → (f : Hom A a  a' ) → Hom ? (id1 A b) f
--- YondaLemma4 {a} {a'} {b} f = Hom A b a →  Hom A b a'
+YonedaLemma4 :  {a a' b : Obj A } (f : Hom A a  a' ) → (g : Hom A b a ) →  Hom A b a' -- f o g
+YonedaLemma4 {a} {a'} {b} f = TMap  (FMap YonedaFunctor  f) b 
 
 --
 -- f ∈ FMap (FObj YonedaFunctor a') a
@@ -312,9 +309,11 @@
 --                 H a ------→ H a'
 --                      H f
 --
+
 _^ : {a a' b : Obj A } → (f : Hom A a  a' )  → Hom A b a →  Hom A b a' 
 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f
 
+
 f-unique : {a a' b : Obj A } (f : Hom A a  a' ) →  f ^ ≡ TMap  (FMap YonedaFunctor  f) b
 f-unique {a} {a'} {b} f  =  extensionality A  (λ g → begin
              (f ^ ) g ≡⟨⟩
@@ -322,124 +321,29 @@
              A [ f o g ] ≡⟨⟩
              TMap  (FMap YonedaFunctor  f) b g ∎  ) where  open ≡-Reasoning 
 
+f-u : {a a' b : Obj A } (f : FObj (FObj YonedaFunctor a') a  ) → Sets [  f ^ ≈   TMap (FMap YonedaFunctor f ) b ]
+f-u = f-unique
+
+
 postulate
-        eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → a ≡ a'
         eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → b ≡ b'
-        eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f'
-        eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g'
-        -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h
 
 open import  Relation.Binary.HeterogeneousEquality as HE using (_≅_) 
 
+-- eqObj2 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b : Obj A}  → Hom A a a ≡ Hom A a b → a ≡ b
+-- eqObj2 A {a} {b}  eq = eqObj3  eq refl where
+--      eqObj3 : {a  b : Obj A} {f : Hom A a a } {g : Hom A b b } → a ≡ b → id1 A a ≅ id1 A b 
+--      eqObj3 refl = HE.refl
+
 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
 a1 HE.refl = refl
 
-eqObj1' :  {a b : Obj A}  → Hom A a a ≡ Hom A a b → a ≡ b
-eqObj1' {a} {b} ha=hb = {!!} where
-        open Small small
-        ylem1 : I
-        ylem1  = hom→ (id1 A a)
-        ylem3 : I → Hom A a b
-        ylem3 i = hom← i
-        ylem2  : (i : I) → hom→ {a} {a} ( subst (λ k → k) (Relation.Binary.PropositionalEquality.sym ha=hb) (hom← {a} {b} i) ) ≡ i
-        ylem2 i = {!!} -- hom-rev
-
-open import Category.Cat
-
-
-≃→a=a : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
-      → ( f : Hom B a b )
-      → ( g : Hom B a' b' )
-      → [_]_~_ B f g → a ≡ a'
-≃→a=a B f g (refl eqv) = refl
-
-≃→b=b : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
-      → ( f : Hom B a b )
-      → ( g : Hom B a' b' )
-      → [_]_~_ B f g → b ≡ b'
-≃→b=b B f g (refl eqv) = refl
-
--- full (injective )
-Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a))  (f : Hom A a b )
-    → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
-    → SetsAop [  g ≈ h ]
-Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z →  ≈-≡ A ( begin
-             TMap g _ z ≈⟨  {!!} ⟩
-             A [ id1 A _ o TMap g _ z ]  ≈⟨  {!!} ⟩
-             ( Sets [ id1 Sets _ o TMap g _ ] ) z  ≈⟨  {!!} ⟩
-             TMap h _ z ∎ ) ) where
-     open ≈-Reasoning A
-     ylem11 : {x : Obj A}  (z : FObj y x) → A [ f  o TMap g _ z ] ≡ A [ f o TMap h _ z ]
-     ylem11  z = (cong (λ k → k z ) yg=yh )
-
--- faithful (surjective)
-Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b )
-    → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ]
-    → SetsAop [  g ≈ h ]
-Yoneda-surjective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z →  ( begin
-             TMap g _ z  ≡⟨ {!!} ⟩
-             TMap g _ (A [ id1 A _ o z ] )  ≡⟨⟩
-             ( Sets [ TMap g _ o FMap (FObj YonedaFunctor b) z ]) (id1 A _) ≡⟨ {!!} ⟩
-             TMap g _ (A [ f  o A [ {!!} o z ] ] )  ≡⟨ {!!} ⟩
-             ( Sets [ FMap y z o TMap g _  ] ) (id1 A _) ≡⟨ {!!} ⟩
-             TMap h _ z ∎ ) ) where
-     open ≡-Reasoning 
-     ylem12 : {y : Obj A} → { z : Hom A y a } → TMap g y (A [ f o z ]) ≡ TMap h y (A [ f o z ])
-     ylem12 {y} {z} = cong (λ k → k z ) (yg=yh {y} )
-     ylem10 : {y : Obj A} → (λ z  → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] ))
-     ylem10 = yg=yh
-
 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
 Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where
      ylem1 : Hom A a a ≡ Hom A a b
      ylem1 = cong (λ k → FObj k a) eq
-
---  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
-
---  Full embedding of Yoneda Functor requires injective on Object, 
---
--- But we cannot prove like this
---     FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
-
-
-open import Relation.Nullary
-open import Data.Empty
-
---YondaLemma2 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
---     (a b x : Obj A )  → (FObj (FObj (YonedaFunctor A) a) x)  ≡ (FObj (FObj (YonedaFunctor A) b ) x)  → a ≡ b 
---YondaLemma2 A a bx eq = {!!}
-
---       N.B     = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b
+     ylem2 : (x : Obj  A) → Category.cod SetsAop (FMap YonedaFunctor (id1 A x)) ≡ FObj YonedaFunctor x
+     ylem2 x = refl
+     ylem3 : {a b : Obj A } →  Hom A a b →  Obj A
+     ylem3 x = Category.cod A x
 
---record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
---  infixr 9 _o_
---  infix  4 _≈_
---  field
---    Obj : Set c₁
---    Hom : Obj → Obj → Set c₂
---YondaLemma31 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
---     (a b x : Obj A )  → Hom A a x  ≡ Hom A b x  → a ≡ b 
---YondaLemma31 A a b x eq = {!!}
---
--- Instead we prove only
---     inv ( FObj YonedaFunctor a )  ≡ a
-
-inv :   {a x : Obj A} ( f : FObj (FObj YonedaFunctor  a) x)  →  Obj A
-inv {a} f =  Category.cod A f
-
-YonedaLemma21 :  {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor  a) x) ) →  inv f  ≡ a
-YonedaLemma21  {a} {x} f = refl
-
--- YondaLemma3 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
---     (a b x : Obj A )  → Hom A a x  ≅ Hom A b x  → a ≡ b 
--- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ?
-
--- a2 :  ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b
--- a2 a b f g eq = {!!}
-
--- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A}
---          → FObj (FObj (YonedaFunctor A ) a ) a  ≅ FObj (FObj (YonedaFunctor A ) a ) b
---          → a ≡ b
--- YonedaInjective A {a} {b} eq = {!!}
-
-