Mercurial > hg > Members > kono > Proof > category

changeset 1001:5861128f1e49

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Mar 2021 12:50:52 +0900
parents 3ef1b472e9f9
children 471f9b977920
files src/yoneda.agda
diffstat 1 files changed, 64 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/yoneda.agda	Tue Mar 09 02:10:14 2021 +0900
+++ b/src/yoneda.agda	Tue Mar 09 12:50:52 2021 +0900
@@ -275,12 +275,10 @@
      → SetsAop [ F2Nat  {a'} {FObj YonedaFunctor  a} f ≈ FMap YonedaFunctor  f ]
 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 
@@ -313,7 +311,6 @@
 _^ : {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 ≡⟨⟩
@@ -324,6 +321,70 @@
 f-u : {a a' b : Obj A } (f : FObj (FObj YonedaFunctor a') a  ) → Sets [  f ^ ≈   TMap (FMap YonedaFunctor f ) b ]
 f-u = f-unique
 
+-- faithful (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 = begin
+             TMap g _ ≈⟨  {!!} ⟩
+             -- {!!} ≈⟨  {!!} ⟩   -- Hom Sets (FObj y x₁) (FObj (FObj YonedaFunctor a) x₁)
+             TMap h _ ∎  where
+     open ≈-Reasoning Sets
+     hoge : (x₁ : Obj A) → FObj y x₁ -- Hom Sets (FObj y x₁) (FObj (FObj YonedaFunctor a) x₁)
+     hoge x₁ = Nat2F {x₁} {y} {!!}
+     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 )
+
+-- full (surjective)
+
+record CatSurjective { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
+         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ')) where
+     field 
+       sur :        {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → Hom A a a'
+       surjective : {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → B [ FMap F (sur g) ≈ g ]
+
+CatEpiR : { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
+    → {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b) 
+    → ( f : Hom A a a' )
+    → (B [ B [ g o FMap F f ] ≈  B [ h o FMap F f ] ] → B [ g  ≈ h ])
+    → CatSurjective A B F 
+CatEpiR A B F g h f eq = record { sur = {!!} ; surjective = {!!} }
+
+CatEpi : { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
+    → CatSurjective A B F
+    → {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b)
+    → ( f : (g h : Hom B (FObj F a') b) → Hom A a a' )
+    → B [ B [ g o FMap F ( f g h ) ] ≈  B [ h o FMap F (f g h ) ] ] → B [ g  ≈ h ]
+CatEpi A B F s g h f gf=hf = begin
+     g ≈⟨ {!!} ⟩
+     h ∎ 
+  where
+     open ≈-Reasoning B
+     sj : B [ FMap F ( CatSurjective.sur s (FMap F (f g h))) ≈ FMap F (f g h) ]
+     sj  = CatSurjective.surjective s (FMap F (f g h)) 
+
+Yoneda-surjective : CatSurjective A SetsAop YonedaFunctor 
+Yoneda-surjective  = record { sur = λ {a} {a'} g → f g ; surjective = λ g → 
+  begin
+     TMap (FMap YonedaFunctor (f g) ) _ ≈⟨ YonedaIso1 g ⟩
+     TMap g _ ∎ 
+ } where
+     open ≈-Reasoning Sets
+     f : {a a' : Obj A } → (g : Hom SetsAop (FObj YonedaFunctor a) (FObj YonedaFunctor a')) → Hom A a a'
+     f g = Nat2F g
+
+-- epi
+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 = begin
+         TMap g _ ≈⟨ {!!} ⟩
+         TMap h _
+         ∎ where
+             open ≈-Reasoning (Sets) 
+             s : CatSurjective A SetsAop YonedaFunctor 
+             s = Yoneda-surjective 
+
 
 postulate
         eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → b ≡ b'