Mercurial > hg > Members > kono > Proof > category

changeset 647:4d261d04b176

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
functorF and η
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2017 03:39:29 +0900
parents 4e0f0105a85d
children 10f2057c8bff
files freyd2.agda
diffstat 1 files changed, 39 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jul 03 20:53:14 2017 +0900
+++ b/freyd2.agda	Tue Jul 04 03:39:29 2017 +0900
@@ -88,13 +88,6 @@
 _↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
          where open import Comma1 F G
 
-natf :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
-    →  { F G : Functor A B }
-    → Functor A B  → Functor A (F ↓ G) → Functor A B
-natf   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } {F} {G} H I = nat-f H I
-         where open import Comma1 F G
-
-open import freyd
 open SmallFullSubcategory
 open Complete
 open PreInitial
@@ -375,6 +368,28 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
+-------------
+-- Adjoint Functor Theorem
+--
+
+tmap-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
+     (U : Functor A B )
+     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
+     (y : Obj B)   → Hom B y (FObj U (obj (i y)))
+tmap-η A B U i y = hom (i y) 
+
+objB : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
+     (U : Functor A B )
+     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
+     (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
+objB A B U i a b f  = record { obj = obj (i b) ; hom = B [ tmap-η A B U i b o f ] }
+
+solution : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
+     (U : Functor A B )
+     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
+     (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
+     (a b  : Obj B)  → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (objB A B U i a b f )
+solution A B U i In a b f =  initial (In a) (objB A B U i a b f )
 
 FunctorF : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
@@ -385,8 +400,8 @@
      (LP :  LimitPreserve A I B U  )
         → Functor B A
 FunctorF A B I comp U SFS PI i In LP = record {
-    FObj = {!!}
-  ; FMap = {!!}
+    FObj = λ b →  obj (i b) 
+  ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB A B U i x y f)) 
   ; isFunctor = record {
              identity =  {!!}
            ; distr = {!!} -- λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
@@ -416,9 +431,23 @@
      (LP :  LimitPreserve A I B U  )
         → NTrans B B identityFunctor (U ○ (FunctorF A B I comp U SFS PI i In LP) )
 nat-η  A B I comp U SFS PI i In LP = 
-      record { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } } where
+      record { TMap = λ y →  tmap-η A B U i y ; isNTrans = record { commute = comm1 } } where
        F : Functor B A
        F = FunctorF A B I comp U SFS PI i In LP
+       comm1 : {a b : Obj B} {f : Hom B a b}
+          → B [ B [ FMap (U ○ FunctorF A B I comp U SFS PI i In LP) f o tmap-η A B U i a ]
+                ≈ B [ tmap-η A B U i b o f ] ]
+       comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
+               FMap (U ○ F) f o tmap-η A B U i a 
+             ≈⟨⟩
+               FMap U ( arrow ( initial (In a) (objB A B U i a b f ))) o hom ( i a )
+             ≈⟨ comm ( initial (In a) (objB A B U i a b f)) ⟩
+               ( tmap-η A B U i b o f ) o FMap (K B A a) (arrow (initial (In a) (objB A B U i a b f)))    
+             ≈⟨ idR ⟩
+               hom (i b ) o f 
+             ≈⟨⟩
+               tmap-η A B U i b o f 
+             ∎ 
 
 IsLeftAdjoint  : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )