Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 50:b518af3a9b07
on goging
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 23 Jul 2013 10:27:24 +0900 |
parents | d2b5be1143bf |
children | adc6bd3c9270 |
rev | line source |
---|---|
31 | 1 module universal-mapping where |
2 | |
3 open import Category -- https://github.com/konn/category-agda | |
4 open import Level | |
5 open import Category.HomReasoning | |
6 | |
7 open Functor | |
37 | 8 |
46 | 9 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
10 id1 A a = (Id {_} {_} {_} {A} a) | |
11 | |
31 | 12 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
13 ( U : Functor B A ) | |
14 ( F : Obj A -> Obj B ) | |
15 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
16 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
17 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
18 field | |
36 | 19 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
37 | 20 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
42 | 21 unique-universalMapping : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (F a') b') -> |
22 A [ A [ FMap U g o η a' ] ≈ f ] -> B [ f * ≈ g ] | |
31 | 23 |
24 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
25 ( U : Functor B A ) | |
26 ( F : Obj A -> Obj B ) | |
27 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
28 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
37 | 29 infixr 11 _* |
31 | 30 field |
37 | 31 _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b |
31 | 32 isUniversalMapping : IsUniversalMapping A B U F η _* |
33 | |
32 | 34 open NTrans |
35 open import Category.Cat | |
36 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
37 ( U : Functor B A ) | |
38 ( F : Functor A B ) | |
39 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
40 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
42 field | |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
43 adjoint1 : { b' : Obj B } -> |
46 | 44 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ id1 A (FObj U b') ] |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
45 adjoint2 : {a' : Obj A} -> |
46 | 46 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ id1 B (FObj F a') ] |
31 | 47 |
32 | 48 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
49 ( U : Functor B A ) | |
50 ( F : Functor A B ) | |
51 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
52 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
53 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
54 field | |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
55 isAdjunction : IsAdjunction A B U F η ε |
32 | 56 |
43 | 57 -- |
58 -- Adjunction yields solution of universal mapping | |
59 -- | |
60 -- | |
61 | |
34 | 62 open Adjunction |
63 open UniversalMapping | |
35 | 64 |
33
fefebc387eae
add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
65 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
35 | 66 ( U : Functor B A ) |
67 ( F : Functor A B ) | |
68 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
69 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
37 | 70 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) |
35 | 71 Lemma1 A B U F η ε adj = record { |
43 | 72 _* = solution ; |
36 | 73 isUniversalMapping = record { |
43 | 74 universalMapping = universalMapping; |
75 unique-universalMapping = uniqness | |
36 | 76 } |
77 } where | |
43 | 78 solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b |
79 solution {_} {b} f = B [ TMap ε b o FMap F f ] | |
37 | 80 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
43 | 81 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] |
38 | 82 universalMapping a b {f} = |
83 let open ≈-Reasoning (A) in | |
84 begin | |
43 | 85 FMap U ( solution f) o TMap η a |
39 | 86 ≈⟨⟩ |
87 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a | |
88 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ | |
89 ( (FMap U (TMap ε b)) o (FMap U ( FMap F f )) ) o TMap η a | |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
90 ≈⟨ sym assoc ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
91 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a ) |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
92 ≈⟨ cdr (nat A η) ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
93 (FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f ) |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
94 ≈⟨ assoc ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
95 ((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
96 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
97 id (FObj U b) o f |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
98 ≈⟨ idL ⟩ |
38 | 99 f |
100 ∎ | |
44 | 101 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g : Hom B (FObj F a) b) -> |
102 A [ A [ FMap U g o TMap η a ] ≈ f ] -> | |
103 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] | |
104 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k | |
43 | 105 uniqness : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (FObj F a') b') -> |
106 A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] | |
44 | 107 uniqness a b f g k = let open ≈-Reasoning (B) in |
108 begin | |
109 solution f | |
110 ≈⟨⟩ | |
111 TMap ε b o FMap F f | |
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
112 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ |
44 | 113 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] ) |
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
114 ≈⟨ cdr (IsFunctor.distr ( isFunctor F )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
115 TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) ) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
116 ≈⟨ assoc ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
117 ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a ) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
118 ≈⟨ sym ( car ( nat B ε )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
119 ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a ) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
120 ≈⟨ sym assoc ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
121 g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) ) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
122 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
123 g o id (FObj F a) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
124 ≈⟨ idR ⟩ |
44 | 125 g |
126 ∎ | |
127 | |
43 | 128 -- |
129 -- | |
130 -- Universal mapping yields Adjunction | |
131 -- | |
132 -- | |
133 | |
134 | |
135 -- | |
136 -- F is an functor | |
137 -- | |
138 | |
41 | 139 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
140 ( U : Functor B A ) | |
141 ( F : Obj A -> Obj B ) | |
142 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
143 UniversalMapping A B U F η -> Functor A B | |
144 FunctorF A B U F η um = record { | |
145 FObj = F; | |
42 | 146 FMap = myFMap ; |
147 isFunctor = myIsFunctor | |
41 | 148 } where |
42 | 149 myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b) |
150 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) | |
46 | 151 lemma-id1 : {a : Obj A} -> A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ] |
152 lemma-id1 {a} = let open ≈-Reasoning (A) in | |
42 | 153 begin |
46 | 154 FMap U (id1 B (F a)) o η a |
42 | 155 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩ |
46 | 156 id (FObj U ( F a )) o η a |
42 | 157 ≈⟨ idL ⟩ |
158 η a | |
159 ≈⟨ sym idR ⟩ | |
46 | 160 η a o id a |
42 | 161 ∎ |
46 | 162 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] |
42 | 163 lemma-id {a} = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) |
46 | 164 a (F a) ((A [ (η a) o (id1 A a)] )) ((id1 B (F a))) lemma-id1 |
165 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → | |
166 A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] | |
167 lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in | |
168 begin | |
169 ( FMap U ((_* um) (A [ η b o g ]) )) o η a | |
170 ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b) ⟩ | |
171 η b o g | |
172 ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ | |
173 η b o f | |
174 ∎ | |
175 lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b o f ] ) ≈ (_* um) (A [ η b o g ]) ] | |
176 lemma-cong1 a b f g eq = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) | |
177 a (F b) (A [ η b o f ]) ((_* um) (A [ η b o g ])) ( lemma-cong2 a b f g eq ) | |
178 lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] | |
179 lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq | |
47 | 180 lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → |
181 A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ]) o η a ] ≈ (A [ η c o A [ g o f ] ]) ] | |
182 lemma-distr2 a b c f g = let open ≈-Reasoning (A) in | |
183 begin | |
184 ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a | |
185 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ | |
186 (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a | |
187 ≈⟨ sym assoc ⟩ | |
188 ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) | |
189 ≈⟨ cdr ( ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b)) ⟩ | |
190 ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) | |
191 ≈⟨ assoc ⟩ | |
192 ( FMap U ((_* um) (A [ η c o g ])) o η b) o f | |
193 ≈⟨ car (( IsUniversalMapping.universalMapping ( isUniversalMapping um )) b (F c)) ⟩ | |
194 ( η c o g ) o f | |
195 ≈⟨ sym assoc ⟩ | |
196 η c o ( g o f ) | |
197 ∎ | |
198 lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → | |
199 B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] | |
200 lemma-distr1 a b c f g = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) a (F c) | |
201 (A [ η c o A [ g o f ] ]) ((B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )) ) (lemma-distr2 a b c f g ) | |
202 lemma-distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )] | |
203 lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g | |
42 | 204 myIsFunctor : IsFunctor A B F myFMap |
205 myIsFunctor = | |
46 | 206 record { ≈-cong = lemma-cong |
42 | 207 ; identity = lemma-id |
47 | 208 ; distr = lemma-distr |
42 | 209 } |
41 | 210 |
48 | 211 -- |
212 -- naturality of η | |
213 -- | |
214 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
215 ( U : Functor B A ) | |
216 ( F : Obj A -> Obj B ) | |
217 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
218 (um : UniversalMapping A B U F η ) -> | |
49 | 219 NTrans A A identityFunctor ( U ○ FunctorF A B U F η um ) |
48 | 220 nat-η A B U F η um = record { |
221 TMap = η ; isNTrans = myIsNTrans | |
222 } where | |
223 F' : Functor A B | |
224 F' = FunctorF A B U F η um | |
225 naturality : {a b : Obj A} {f : Hom A a b} | |
226 → A [ A [ (FMap U (FMap F' f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] | |
49 | 227 naturality {a} {b} {f} = let open ≈-Reasoning (A) in |
228 begin | |
229 (FMap U (FMap F' f)) o ( η a ) | |
230 ≈⟨⟩ | |
231 (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) | |
232 ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) a ( F b ) ⟩ | |
233 (η b ) o f | |
234 ∎ | |
48 | 235 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η |
236 myIsNTrans = record { naturality = naturality } | |
49 | 237 |
238 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
239 ( U : Functor B A ) | |
240 ( F : Obj A -> Obj B ) | |
241 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
242 (um : UniversalMapping A B U F η ) -> | |
243 NTrans B B ( FunctorF A B U F η um ○ U) identityFunctor | |
244 nat-ε A B U F η um = record { | |
245 TMap = ε ; isNTrans = myIsNTrans | |
246 } where | |
247 F' : Functor A B | |
248 F' = FunctorF A B U F η um | |
249 ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b | |
250 ε b = (_* um) ( id1 A (FObj U b)) | |
251 naturality : {a b : Obj B} {f : Hom B a b } | |
252 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ] | |
253 naturality {a} {b} {f} = let open ≈-Reasoning (B) in | |
254 sym ( begin | |
255 ε b o (FMap F' (FMap U f)) | |
256 ≈⟨⟩ | |
50 | 257 ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) |
258 ≈⟨⟩ | |
259 ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) | |
49 | 260 ≈⟨ {!!} ⟩ |
50 | 261 f o ((_* um) ( id1 A (FObj U a))) |
262 ≈⟨⟩ | |
49 | 263 f o (ε a) |
264 ∎ ) | |
265 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε | |
266 myIsNTrans = record { naturality = naturality } |