Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 49:d2b5be1143bf
naturality of ε
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 10:13:09 +0900 |
| parents | d5a8edad2a83 |
| children | b518af3a9b07 |
| 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 ≈⟨⟩ | |
| 257 ε b o (FMap F' (FMap U f)) | |
| 258 ≈⟨ {!!} ⟩ | |
| 259 f o (ε a) | |
| 260 ∎ ) | |
| 261 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε | |
| 262 myIsNTrans = record { naturality = naturality } |