Mercurial > hg > Members > kono > Proof > category
annotate freyd.agda @ 441:61550782be4a
preinital full subcategory done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 30 Aug 2016 15:11:17 +0900 |
parents | ff36c500962e |
children | 87600d338337 |
rev | line source |
---|---|
304
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 where |
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
307
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
7 open import cat-utility |
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
8 open import HomReasoning |
304
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Relation.Binary.Core |
307
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
10 open Functor |
304
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
311 | 12 -- C is small full subcategory of A ( C is image of F ) |
304
bd7b3f3d1d4c
Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
307
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b ) |
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where |
306
92475fe5f59e
Small Full Subcategory (underconstruction)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
305
diff
changeset
|
17 field |
307
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } → |
436
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- codomain of FMap is local small |
307
9872bddec072
small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
306
diff
changeset
|
20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ] |
305 | 21 |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
22 -- pre-initial |
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
23 |
311 | 24 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
25 (F : Functor A A ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where | |
308 | 26 field |
314 | 27 preinitialObj : ∀{ a : Obj A } → Obj A |
28 preinitialArrow : ∀{ a : Obj A } → Hom A ( FObj F (preinitialObj {a} )) a | |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
29 |
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
30 -- initial object |
308 | 31 |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
32 record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where |
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
33 field |
314 | 34 initial : ∀( a : Obj A ) → Hom A i a |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
35 uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ] |
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
36 |
315 | 37 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
38 |
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
39 open NTrans |
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
40 open Limit |
313 | 41 open SmallFullSubcategory |
42 open PreInitial | |
440 | 43 open Complete |
44 open Equalizer | |
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
45 |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
46 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
47 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b ) |
440 | 48 (comp : Complete A A) |
309
e213595b845e
preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
308
diff
changeset
|
49 (SFS : SmallFullSubcategory A F FMap← ) → |
440 | 50 (PI : PreInitial A F ) → { a0 : Obj A } → HasInitialObject A (limit-c comp F) |
51 initialFromPreInitialFullSubcategory A F FMap← comp SFS PI = record { | |
314 | 52 initial = initialArrow ; |
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
53 uniqueness = λ a f → lemma1 a f |
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
311
diff
changeset
|
54 } where |
440 | 55 lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ) |
56 lim Γ = isLimit comp Γ | |
57 equ : {a b : Obj A} → (f g : Hom A a b) → Equalizer A (equalizer-e comp f g ) f g | |
58 equ f g = isEqualizer comp f g | |
59 a0 = limit-c comp F | |
60 u = limit-u comp F | |
61 ee : {a b : Obj A} → {f g : Hom A a b} → Obj A | |
62 ee {a} {b} {f} {g} = equalizer-p comp f g | |
63 ep : {a b : Obj A} → {f g : Hom A a b} → Hom A (ee {a} {b} {f} {g} ) a | |
64 ep {a} {b} {f} {g} = equalizer-e comp f g | |
437 | 65 f : {a : Obj A} -> Hom A a0 (FObj F (preinitialObj PI {a} ) ) |
440 | 66 f {a} = TMap u (preinitialObj PI {a} ) |
314 | 67 initialArrow : ∀( a : Obj A ) → Hom A a0 a |
437 | 68 initialArrow a = A [ preinitialArrow PI {a} o f ] |
440 | 69 equ-fi : { a : Obj A} -> {f' : Hom A a0 a} -> |
70 Equalizer A ep ( A [ preinitialArrow PI {a} o f ] ) f' | |
71 equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f' | |
72 e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap u c o e ] ≈ TMap u c ] ) -> A [ e ≈ id1 A a0 ] | |
438 | 73 e=id {e} uce=uc = let open ≈-Reasoning (A) in |
437 | 74 begin |
75 e | |
440 | 76 ≈↑⟨ limit-uniqueness (lim F) e ( \{i} -> uce=uc ) ⟩ |
77 limit (lim F) a0 u | |
78 ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( \{i} -> idR ) ⟩ | |
437 | 79 id1 A a0 |
80 ∎ | |
440 | 81 kfuc=uc : {c k1 : Obj A} -> {p : Hom A k1 a0} -> A [ A [ TMap u c o |
82 A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ] | |
83 ≈ TMap u c ] | |
441
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
84 kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
85 begin |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
86 TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) )) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
87 ≈⟨ cdr assoc ⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
88 TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI)) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
89 ≈⟨ assoc ⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
90 (TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
91 ≈↑⟨ car ( full→ SFS ) ⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
92 FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
93 ≈⟨ nat u ⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
94 TMap u c o FMap (K A A (limit-c comp F)) (FMap← (TMap u c o p o preinitialArrow PI)) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
95 ≈⟨⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
96 TMap u c o id1 A (limit-c comp F) |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
97 ≈⟨ idR ⟩ |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
98 TMap u c |
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
99 ∎ |
440 | 100 kfuc=1 : {k1 : Obj A} -> {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ] |
439 | 101 kfuc=1 {k1} {p} = e=id ( kfuc=uc ) |
435
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
102 -- if equalizer has right inverse, f = g |
438 | 103 lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) |
104 {e : Hom A c a } {e' : Hom A a c } ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] ) | |
435
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
105 -> A [ f ≈ g ] |
438 | 106 lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in |
435
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
107 let open Equalizer in |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
108 begin |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
109 f |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
110 ≈↑⟨ idR ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
111 f o id1 A a |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
112 ≈↑⟨ cdr inv-e ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
113 f o ( e o e' ) |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
114 ≈⟨ assoc ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
115 ( f o e ) o e' |
441
61550782be4a
preinital full subcategory done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
440
diff
changeset
|
116 ≈⟨ car ( fe=ge equ ) ⟩ ( g o e ) o e' |
435
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
117 ≈↑⟨ assoc ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
118 g o ( e o e' ) |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
119 ≈⟨ cdr inv-e ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
120 g o id1 A a |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
121 ≈⟨ idR ⟩ |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
122 g |
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
123 ∎ |
439 | 124 lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ] |
438 | 125 lemma1 a f' = let open ≈-Reasoning (A) in |
436
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
126 sym ( |
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
127 begin |
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
128 initialArrow a |
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
129 ≈⟨⟩ |
440 | 130 preinitialArrow PI {a} o f |
131 ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o f ]) f' {ep {a0} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) | |
439 | 132 (kfuc=1 {ee} {ep} ) ⟩ |
438 | 133 f' |
436
ef37decef1ca
initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
435
diff
changeset
|
134 ∎ ) |
435
9f014f34b988
f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
350
diff
changeset
|
135 |