Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 171:d25b0948e006
unity of oppsite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Aug 2013 10:11:58 +0900 |
| parents | 0be3e0a49cca |
| children | c7fef385330f |
| rev | line source |
|---|---|
| 31 | 1 module universal-mapping where |
| 2 | |
| 56 | 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
| 4 | |
| 31 | 5 open import Category -- https://github.com/konn/category-agda |
| 6 open import Level | |
| 56 | 7 open import HomReasoning |
| 159 | 8 open import cat-utility |
| 9 open import Category.Cat | |
| 31 | 10 |
| 11 open Functor | |
| 32 | 12 open NTrans |
| 13 | |
| 43 | 14 -- |
| 15 -- Adjunction yields solution of universal mapping | |
| 16 -- | |
| 17 -- | |
| 18 | |
| 34 | 19 open Adjunction |
| 20 open UniversalMapping | |
| 35 | 21 |
| 56 | 22 Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 54 | 23 { U : Functor B A } |
| 24 { F : Functor A B } | |
| 25 { η : NTrans A A identityFunctor ( U ○ F ) } | |
| 56 | 26 { ε : NTrans B B ( F ○ U ) identityFunctor } → |
| 27 Adjunction A B U F η ε → UniversalMapping A B U (FObj F) (TMap η) | |
| 28 Adj2UM A B {U} {F} {η} {ε} adj = record { | |
| 43 | 29 _* = solution ; |
| 36 | 30 isUniversalMapping = record { |
| 43 | 31 universalMapping = universalMapping; |
| 51 | 32 uniquness = uniqness |
| 36 | 33 } |
| 34 } where | |
| 56 | 35 solution : { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) → Hom B (FObj F a ) b |
| 43 | 36 solution {_} {b} f = B [ TMap ε b o FMap F f ] |
| 56 | 37 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → |
| 43 | 38 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] |
| 51 | 39 universalMapping {a} {b} {f} = |
| 38 | 40 let open ≈-Reasoning (A) in |
| 41 begin | |
| 43 | 42 FMap U ( solution f) o TMap η a |
| 39 | 43 ≈⟨⟩ |
| 44 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a | |
| 66 | 45 ≈⟨ car (distr U ) ⟩ |
| 39 | 46 ( (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
|
47 ≈⟨ sym assoc ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
48 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a ) |
| 66 | 49 ≈⟨ cdr (nat η) ⟩ |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
50 (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
|
51 ≈⟨ assoc ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
52 ((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
|
53 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
54 id (FObj U b) o f |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
55 ≈⟨ idL ⟩ |
| 38 | 56 f |
| 57 ∎ | |
| 56 | 58 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g : Hom B (FObj F a) b) → |
| 59 A [ A [ FMap U g o TMap η a ] ≈ f ] → | |
| 44 | 60 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] |
| 61 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k | |
| 56 | 62 uniqness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} → |
| 63 A [ A [ FMap U g o TMap η a' ] ≈ f ] → B [ solution f ≈ g ] | |
| 52 | 64 uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in |
| 44 | 65 begin |
| 66 solution f | |
| 67 ≈⟨⟩ | |
| 68 TMap ε b o FMap F f | |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
69 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ |
| 44 | 70 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] ) |
| 66 | 71 ≈⟨ cdr (distr F ) ⟩ |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
72 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
|
73 ≈⟨ assoc ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
74 ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a ) |
| 66 | 75 ≈⟨ sym ( car ( nat ε )) ⟩ |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
76 ( 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
|
77 ≈⟨ sym assoc ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
78 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
|
79 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
80 g o id (FObj F a) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
81 ≈⟨ idR ⟩ |
| 44 | 82 g |
| 83 ∎ | |
| 84 | |
| 43 | 85 -- |
| 86 -- | |
| 87 -- Universal mapping yields Adjunction | |
| 88 -- | |
| 89 -- | |
| 90 | |
| 91 | |
| 92 -- | |
| 93 -- F is an functor | |
| 94 -- | |
| 95 | |
| 54 | 96 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 97 { U : Functor B A } | |
| 56 | 98 { F : Obj A → Obj B } |
| 99 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 100 UniversalMapping A B U F η → Functor A B | |
| 54 | 101 FunctorF A B {U} {F} {η} um = record { |
| 41 | 102 FObj = F; |
| 42 | 103 FMap = myFMap ; |
| 104 isFunctor = myIsFunctor | |
| 41 | 105 } where |
| 56 | 106 myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b) |
| 42 | 107 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) |
| 56 | 108 lemma-id1 : {a : Obj A} → A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ] |
| 46 | 109 lemma-id1 {a} = let open ≈-Reasoning (A) in |
| 42 | 110 begin |
| 46 | 111 FMap U (id1 B (F a)) o η a |
| 42 | 112 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩ |
| 46 | 113 id (FObj U ( F a )) o η a |
| 42 | 114 ≈⟨ idL ⟩ |
| 115 η a | |
| 116 ≈⟨ sym idR ⟩ | |
| 46 | 117 η a o id a |
| 42 | 118 ∎ |
| 46 | 119 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] |
| 52 | 120 lemma-id {a} = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) lemma-id1 |
| 46 | 121 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → |
| 122 A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] | |
| 123 lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in | |
| 124 begin | |
| 125 ( FMap U ((_* um) (A [ η b o g ]) )) o η a | |
| 51 | 126 ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 46 | 127 η b o g |
| 128 ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ | |
| 129 η b o f | |
| 130 ∎ | |
| 131 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 ]) ] | |
| 52 | 132 lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) ( lemma-cong2 a b f g eq ) |
| 46 | 133 lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] |
| 134 lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq | |
| 47 | 135 lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → |
| 136 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 ] ]) ] | |
| 137 lemma-distr2 a b c f g = let open ≈-Reasoning (A) in | |
| 138 begin | |
| 139 ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a | |
| 66 | 140 ≈⟨ car (distr U ) ⟩ |
| 47 | 141 (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a |
| 142 ≈⟨ sym assoc ⟩ | |
| 143 ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) | |
| 51 | 144 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 145 ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) |
| 146 ≈⟨ assoc ⟩ | |
| 147 ( FMap U ((_* um) (A [ η c o g ])) o η b) o f | |
| 51 | 148 ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 149 ( η c o g ) o f |
| 150 ≈⟨ sym assoc ⟩ | |
| 151 η c o ( g o f ) | |
| 152 ∎ | |
| 153 lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → | |
| 154 B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] | |
| 52 | 155 lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( isUniversalMapping um )) (lemma-distr2 a b c f g ) |
| 47 | 156 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 ] )] |
| 157 lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g | |
| 42 | 158 myIsFunctor : IsFunctor A B F myFMap |
| 159 myIsFunctor = | |
| 46 | 160 record { ≈-cong = lemma-cong |
| 42 | 161 ; identity = lemma-id |
| 47 | 162 ; distr = lemma-distr |
| 42 | 163 } |
| 41 | 164 |
| 48 | 165 -- |
| 166 -- naturality of η | |
| 167 -- | |
| 168 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 54 | 169 { U : Functor B A } |
| 56 | 170 { F : Obj A → Obj B } |
| 171 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 172 (um : UniversalMapping A B U F η ) → | |
| 54 | 173 NTrans A A identityFunctor ( U ○ FunctorF A B um ) |
| 174 nat-η A B {U} {F} {η} um = record { | |
| 48 | 175 TMap = η ; isNTrans = myIsNTrans |
| 176 } where | |
| 177 F' : Functor A B | |
| 54 | 178 F' = FunctorF A B um |
| 130 | 179 commute : {a b : Obj A} {f : Hom A a b} |
| 48 | 180 → A [ A [ (FMap U (FMap F' f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] |
| 130 | 181 commute {a} {b} {f} = let open ≈-Reasoning (A) in |
| 49 | 182 begin |
| 183 (FMap U (FMap F' f)) o ( η a ) | |
| 184 ≈⟨⟩ | |
| 185 (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) | |
| 51 | 186 ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 49 | 187 (η b ) o f |
| 188 ∎ | |
| 48 | 189 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η |
| 130 | 190 myIsNTrans = record { commute = commute } |
| 49 | 191 |
| 192 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 54 | 193 { U : Functor B A } |
| 56 | 194 { F : Obj A → Obj B } |
| 195 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 196 (um : UniversalMapping A B U F η ) → | |
| 54 | 197 NTrans B B ( FunctorF A B um ○ U) identityFunctor |
| 198 nat-ε A B {U} {F} {η} um = record { | |
| 49 | 199 TMap = ε ; isNTrans = myIsNTrans |
| 200 } where | |
| 201 F' : Functor A B | |
| 54 | 202 F' = FunctorF A B um |
| 56 | 203 ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b |
| 49 | 204 ε b = (_* um) ( id1 A (FObj U b)) |
| 56 | 205 lemma-nat1 : (a b : Obj B) (f : Hom B a b ) → |
| 51 | 206 A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] ) o η (FObj U a) ] |
| 207 ≈ A [ FMap U f o id1 A (FObj U a) ] ] | |
| 208 lemma-nat1 a b f = let open ≈-Reasoning (A) in | |
| 209 begin | |
| 210 FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] ) o η (FObj U a) | |
| 66 | 211 ≈⟨ car ( distr U ) ⟩ |
| 51 | 212 ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a) |
| 213 ≈⟨ sym assoc ⟩ | |
| 214 FMap U ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f ))) o η (FObj U a) | |
| 215 ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 216 FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f ) | |
| 217 ≈⟨ assoc ⟩ | |
| 218 (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f | |
| 219 ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 220 id1 A (FObj U b) o FMap U f | |
| 221 ≈⟨ idL ⟩ | |
| 222 FMap U f | |
| 223 ≈⟨ sym idR ⟩ | |
| 224 FMap U f o id (FObj U a) | |
| 225 ∎ | |
| 56 | 226 lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ] |
| 52 | 227 ≈ A [ FMap U f o id1 A (FObj U a) ] ] |
| 228 lemma-nat2 a b f = let open ≈-Reasoning (A) in | |
| 229 begin | |
| 230 FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ]) o η (FObj U a) | |
| 66 | 231 ≈⟨ car ( distr U ) ⟩ |
| 52 | 232 (FMap U f o FMap U ((um *) (id1 A (FObj U a )))) o η (FObj U a) |
| 233 ≈⟨ sym assoc ⟩ | |
| 234 FMap U f o ( FMap U ((um *) (id1 A (FObj U a ))) o η (FObj U a) ) | |
| 235 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ | |
| 236 FMap U f o id (FObj U a ) | |
| 237 ∎ | |
| 130 | 238 commute : {a b : Obj B} {f : Hom B a b } |
| 49 | 239 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ] |
| 130 | 240 commute {a} {b} {f} = let open ≈-Reasoning (B) in |
| 49 | 241 sym ( begin |
| 242 ε b o (FMap F' (FMap U f)) | |
| 243 ≈⟨⟩ | |
| 50 | 244 ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) |
| 245 ≈⟨⟩ | |
| 246 ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) | |
| 52 | 247 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat1 a b f))) ⟩ |
| 51 | 248 (_* um) ( A [ FMap U f o id1 A (FObj U a) ] ) |
| 52 | 249 ≈⟨ (IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat2 a b f)) ⟩ |
| 50 | 250 f o ((_* um) ( id1 A (FObj U a))) |
| 251 ≈⟨⟩ | |
| 49 | 252 f o (ε a) |
| 253 ∎ ) | |
| 254 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε | |
| 130 | 255 myIsNTrans = record { commute = commute } |
| 53 | 256 |
| 257 ------ | |
| 258 -- | |
| 259 -- Adjunction Construction from Universal Mapping | |
| 260 -- | |
| 261 ----- | |
| 262 | |
| 263 UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 264 ( U : Functor B A ) | |
| 56 | 265 ( F' : Obj A → Obj B ) |
| 266 ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) → | |
| 267 (um : UniversalMapping A B U F' η' ) → | |
| 54 | 268 Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B um) |
| 53 | 269 UMAdjunction A B U F' η' um = record { |
| 270 isAdjunction = record { | |
| 271 adjoint1 = adjoint1 ; | |
| 272 adjoint2 = adjoint2 | |
| 273 } | |
| 274 } where | |
| 275 F : Functor A B | |
| 54 | 276 F = FunctorF A B um |
| 53 | 277 η : NTrans A A identityFunctor ( U ○ F ) |
| 54 | 278 η = nat-η A B um |
| 53 | 279 ε : NTrans B B ( F ○ U ) identityFunctor |
| 54 | 280 ε = nat-ε A B um |
| 56 | 281 adjoint1 : { b : Obj B } → |
| 53 | 282 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
283 adjoint1 {b} = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
284 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
285 FMap U ( TMap ε b ) o TMap η ( FObj U b ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
286 ≈⟨⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
287 FMap U ((_* um) ( id1 A (FObj U b))) o η' ( FObj U b ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
288 ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um ) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
289 id (FObj U b) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
290 ∎ |
| 56 | 291 lemma-adj1 : (a : Obj A) → |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
292 A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ] |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
293 ≈ (η' a) ] |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
294 lemma-adj1 a = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
295 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
296 FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a |
| 66 | 297 ≈⟨ car (distr U) ⟩ |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
298 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
299 ≈⟨ sym assoc ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
300 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
301 ≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
302 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
303 ≈⟨ assoc ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
304 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
305 ≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
306 id (FObj U ( FObj F a)) o ( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
307 ≈⟨ idL ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
308 η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
309 ∎ |
| 56 | 310 lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈ η' a ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
311 lemma-adj2 a = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
312 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
313 FMap U (id1 B (FObj F a)) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
314 ≈⟨ car ( IsFunctor.identity ( isFunctor U)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
315 id (FObj U (FObj F a)) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
316 ≈⟨ idL ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
317 η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
318 ∎ |
| 56 | 319 adjoint2 : {a : Obj A} → |
| 53 | 320 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
321 adjoint2 {a} = let open ≈-Reasoning (B) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
322 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
323 TMap ε ( FObj F a ) o FMap F ( TMap η a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
324 ≈⟨⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
325 ((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
326 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj1 a))) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
327 (_* um)( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
328 ≈⟨ IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj2 a) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
329 id1 B (FObj F a) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
330 ∎ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
331 |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
332 |
| 171 | 333 ------ |
| 334 -- | |
| 335 -- Hom(F(-),-) = Hom(-,U(-)) | |
| 336 -- Unity of opposite | |
| 337 ----- | |
| 338 | |
| 339 Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 340 { U : Functor B A } | |
| 341 { F : Functor A B } | |
| 342 { η : NTrans A A identityFunctor ( U ○ F ) } | |
| 343 { ε : NTrans B B ( F ○ U ) identityFunctor } → | |
| 344 ( adj : Adjunction A B U F η ε ) → UnityOfOppsite A B U F | |
| 345 Adj2UO A B {U} {F} {η} {ε} adj = record { | |
| 346 right = right ; | |
| 347 left = left ; | |
| 348 right-injective = right-injective ; | |
| 349 left-injective = left-injective | |
| 350 } where | |
| 351 right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b | |
| 352 right {a} {b} f = B [ TMap ε b o FMap F f ] | |
| 353 left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) | |
| 354 left {a} {b} f = A [ FMap U f o (TMap η a) ] | |
| 355 right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] | |
| 356 right-injective {a} {b} {f} = let open ≈-Reasoning (A) in | |
| 357 begin | |
| 358 FMap U (B [ TMap ε b o FMap F f ]) o (TMap η a) | |
| 359 ≈⟨ car ( distr U ) ⟩ | |
| 360 ( FMap U (TMap ε b) o FMap U (FMap F f )) o (TMap η a) | |
| 361 ≈↑⟨ assoc ⟩ | |
| 362 FMap U (TMap ε b) o ( FMap U (FMap F f ) o (TMap η a) ) | |
| 363 ≈⟨ cdr ( nat η) ⟩ | |
| 364 FMap U (TMap ε b) o ((TMap η (FObj U b)) o f ) | |
| 365 ≈⟨ assoc ⟩ | |
| 366 (FMap U (TMap ε b) o (TMap η (FObj U b))) o f | |
| 367 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj )) ⟩ | |
| 368 id1 A (FObj U b) o f | |
| 369 ≈⟨ idL ⟩ | |
| 370 f | |
| 371 ∎ | |
| 372 left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] | |
| 373 left-injective {a} {b} {f} = let open ≈-Reasoning (B) in | |
| 374 begin | |
| 375 TMap ε b o FMap F ( A [ FMap U f o (TMap η a) ]) | |
| 376 ≈⟨ cdr ( distr F ) ⟩ | |
| 377 TMap ε b o ( FMap F (FMap U f) o FMap F (TMap η a)) | |
| 378 ≈⟨ assoc ⟩ | |
| 379 ( TMap ε b o FMap F (FMap U f)) o FMap F (TMap η a) | |
| 380 ≈↑⟨ car (nat ε) ⟩ | |
| 381 ( f o TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) | |
| 382 ≈↑⟨ assoc ⟩ | |
| 383 f o ( TMap ε ( FObj F a ) o ( FMap F ( TMap η a ))) | |
| 384 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ | |
| 385 f o id1 B (FObj F a) | |
| 386 ≈⟨ idR ⟩ | |
| 387 f | |
| 388 ∎ | |
| 389 | |
| 390 open UnityOfOppsite | |
| 391 | |
| 392 uo-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} | |
| 393 { U : Functor B A } | |
| 394 { F : Functor A B } → | |
| 395 ( uo : UnityOfOppsite A B U F) → NTrans A A identityFunctor ( U ○ F ) | |
| 396 uo-η {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo = record { | |
| 397 TMap = η ; isNTrans = myIsNTrans | |
| 398 } where | |
| 399 η : (a : Obj A) → Hom A a ( FObj U (FObj F a) ) | |
| 400 η a = left uo ( id1 B (FObj F a) ) | |
| 401 commute : {a b : Obj A} {f : Hom A a b} | |
| 402 → A [ A [ (FMap U (FMap F f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] | |
| 403 commute {a} {b} {f} = let open ≈-Reasoning (A) in | |
| 404 begin | |
| 405 (FMap U (FMap F f)) o ( η a ) | |
| 406 ≈⟨⟩ | |
| 407 (FMap U (FMap F f)) o left uo ( id1 B (FObj F a) ) | |
| 408 ≈⟨ {!!} ⟩ | |
| 409 left uo ( id1 B (FObj F b)) o f | |
| 410 ≈⟨⟩ | |
| 411 (η b ) o f | |
| 412 ∎ | |
| 413 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F ) η | |
| 414 myIsNTrans = record { commute = commute } | |
| 415 | |
| 416 UO2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} | |
| 417 { U : Functor B A } | |
| 418 { F : Functor A B } → | |
| 419 ( uo : UnityOfOppsite A B U F) → UniversalMapping A B U (FObj F) (TMap (uo-η uo) ) | |
| 420 UO2UM = {!!} | |
| 421 | |
| 422 uo-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} | |
| 423 { U : Functor B A } | |
| 424 { F : Functor A B }→ | |
| 425 ( uo : UnityOfOppsite A B U F) → NTrans B B ( F ○ U ) identityFunctor | |
| 426 uo-ε = {!!} | |
| 427 | |
| 428 UO2Adj : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 429 { U : Functor B A } | |
| 430 { F : Functor A B } | |
| 431 ( uo : UnityOfOppsite A B U F) → Adjunction A B U F (uo-η uo ) (uo-ε uo ) | |
| 432 UO2Adj A B {U} {F} uo = record { | |
| 433 isAdjunction = record { | |
| 434 adjoint1 = adjoint1 ; | |
| 435 adjoint2 = adjoint2 | |
| 436 } | |
| 437 } where | |
| 438 adjoint1 : { b : Obj B } → | |
| 439 A [ A [ ( FMap U ( TMap (uo-ε uo) b )) o ( TMap (uo-η uo) ( FObj U b )) ] ≈ id1 A (FObj U b) ] | |
| 440 adjoint1 {b} = {!!} | |
| 441 adjoint2 : {a : Obj A} → | |
| 442 B [ B [ ( TMap (uo-ε uo) ( FObj F a )) o ( FMap F ( TMap (uo-η uo) a )) ] ≈ id1 B (FObj F a) ] | |
| 443 adjoint2 {a} = {!!} | |
| 444 | |
| 445 | |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
446 -- done! |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
447 |