Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 45:659b8a21caf7
uniq-univeralMapping from Adjunction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 23 Jul 2013 01:45:56 +0900 |
parents | a626fdd909c3 |
children | 5d1b0fd2ad21 |
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 |
31 | 9 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
10 ( U : Functor B A ) | |
11 ( F : Obj A -> Obj B ) | |
12 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
13 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
14 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
15 field | |
36 | 16 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
37 | 17 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
42 | 18 unique-universalMapping : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (F a') b') -> |
19 A [ A [ FMap U g o η a' ] ≈ f ] -> B [ f * ≈ g ] | |
31 | 20 |
21 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
22 ( U : Functor B A ) | |
23 ( F : Obj A -> Obj B ) | |
24 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
25 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
37 | 26 infixr 11 _* |
31 | 27 field |
37 | 28 _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b |
31 | 29 isUniversalMapping : IsUniversalMapping A B U F η _* |
30 | |
32 | 31 open NTrans |
32 open import Category.Cat | |
33 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
34 ( U : Functor B A ) | |
35 ( F : Functor A B ) | |
36 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
37 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
38 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
39 field | |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
40 adjoint1 : { b' : Obj B } -> |
32 | 41 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ] |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
42 adjoint2 : {a' : Obj A} -> |
32 | 43 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ Id {_} {_} {_} {B} (FObj F a') ] |
31 | 44 |
32 | 45 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
46 ( U : Functor B A ) | |
47 ( F : Functor A B ) | |
48 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
49 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
50 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
51 field | |
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
52 isAdjunction : IsAdjunction A B U F η ε |
32 | 53 |
43 | 54 -- |
55 -- Adjunction yields solution of universal mapping | |
56 -- | |
57 -- | |
58 | |
34 | 59 open Adjunction |
60 open UniversalMapping | |
35 | 61 |
33
fefebc387eae
add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
62 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
35 | 63 ( U : Functor B A ) |
64 ( F : Functor A B ) | |
65 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
66 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
37 | 67 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) |
35 | 68 Lemma1 A B U F η ε adj = record { |
43 | 69 _* = solution ; |
36 | 70 isUniversalMapping = record { |
43 | 71 universalMapping = universalMapping; |
72 unique-universalMapping = uniqness | |
36 | 73 } |
74 } where | |
43 | 75 solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b |
76 solution {_} {b} f = B [ TMap ε b o FMap F f ] | |
37 | 77 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
43 | 78 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] |
38 | 79 universalMapping a b {f} = |
80 let open ≈-Reasoning (A) in | |
81 begin | |
43 | 82 FMap U ( solution f) o TMap η a |
39 | 83 ≈⟨⟩ |
84 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a | |
85 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ | |
86 ( (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
|
87 ≈⟨ sym assoc ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
88 (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
|
89 ≈⟨ cdr (nat A η) ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
90 (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
|
91 ≈⟨ assoc ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
92 ((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
|
93 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
94 id (FObj U b) o f |
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
95 ≈⟨ idL ⟩ |
38 | 96 f |
97 ∎ | |
44 | 98 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g : Hom B (FObj F a) b) -> |
99 A [ A [ FMap U g o TMap η a ] ≈ f ] -> | |
100 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] | |
101 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k | |
43 | 102 uniqness : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (FObj F a') b') -> |
103 A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] | |
44 | 104 uniqness a b f g k = let open ≈-Reasoning (B) in |
105 begin | |
106 solution f | |
107 ≈⟨⟩ | |
108 TMap ε b o FMap F f | |
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
109 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ |
44 | 110 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
|
111 ≈⟨ cdr (IsFunctor.distr ( isFunctor F )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
112 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
|
113 ≈⟨ assoc ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
114 ( 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
|
115 ≈⟨ sym ( car ( nat B ε )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
116 ( 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
|
117 ≈⟨ sym assoc ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
118 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
|
119 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
120 g o id (FObj F a) |
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
121 ≈⟨ idR ⟩ |
44 | 122 g |
123 ∎ | |
124 | |
43 | 125 -- |
126 -- | |
127 -- Universal mapping yields Adjunction | |
128 -- | |
129 -- | |
130 | |
131 | |
132 -- | |
133 -- F is an functor | |
134 -- | |
135 | |
41 | 136 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
137 ( U : Functor B A ) | |
138 ( F : Obj A -> Obj B ) | |
139 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
140 UniversalMapping A B U F η -> Functor A B | |
141 FunctorF A B U F η um = record { | |
142 FObj = F; | |
42 | 143 FMap = myFMap ; |
144 isFunctor = myIsFunctor | |
41 | 145 } where |
42 | 146 myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b) |
147 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) | |
148 lemma-id-1 : {a : Obj A} -> A [ A [ FMap U (Id {_} {_} {_} {B} (F a)) o η a ] ≈ (A [ (η a) o (Id {_} {_} {_} {A} a) ]) ] | |
149 lemma-id-1 {a} = let open ≈-Reasoning (A) in | |
150 begin | |
151 A [ FMap U (Id {_} {_} {_} {B} (F a)) o η a ] | |
152 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩ | |
153 A [ (Id {_} {_} {_} {A} (FObj U ( F a )) ) o η a ] | |
154 ≈⟨ idL ⟩ | |
155 η a | |
156 ≈⟨ sym idR ⟩ | |
157 (A [ (η a) o (Id {_} {_} {_} {A} a) ]) | |
158 ∎ | |
159 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (Id {_} {_} {_} {A} a)] )) ≈ (Id {_} {_} {_} {B} (F a)) ] | |
160 lemma-id {a} = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) | |
161 a (F a) ((A [ (η a) o (Id {_} {_} {_} {A} a)] )) ((Id {_} {_} {_} {B} (F a))) lemma-id-1 | |
162 myIsFunctor : IsFunctor A B F myFMap | |
163 myIsFunctor = | |
164 record { ≈-cong = {!!} | |
165 ; identity = lemma-id | |
166 ; distr = {!!} | |
167 } | |
41 | 168 |