1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
(** We prove the equivalence of the two definitions of adjunction. *)
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories
MathClasses.misc.workaround_tactics MathClasses.theory.jections.
Require MathClasses.categories.dual.
Local Hint Unfold id compose: typeclass_instances. (* todo: move *)
Local Existing Instance injective_mor.
Local Existing Instance surjective_mor.
Lemma equal_because_sole `{Setoid T} (P: T → Prop) x: is_sole P x → forall y z, P y → P z → y = z.
Proof. firstorder. Qed. (* todo: move *)
Section for_φAdjunction.
(* MacLane p79/p80, showing that from an φAdjunction we can make
both a ηAdjunction and a ηεAdjunction. *)
Context `(φAdjunction).
Arguments φ {_ _} _.
Instance: forall c d, Bijective (@φ c d) := φ_adjunction_bijective F G.
Instance: Functor F F' := φ_adjunction_left_functor F G.
Instance: Functor G G' := φ_adjunction_right_functor F G.
Instance: Category D := functor_from G.
Instance: Category C := functor_to G.
(* Waiting for the new proof engine ... *)
Lemma φ_adjunction_natural_right_inv `(g: c ⟶ G d) `(h: c' ⟶ c): φ⁻¹ (g ◎ h) = φ⁻¹ g ◎ fmap F h.
Proof with try reflexivity; try apply _.
intros.
apply (injective φ).
rewrite surjective_applied...
rewrite φ_adjunction_natural_right...
rewrite surjective_applied...
Qed.
Lemma φ_adjunction_natural_left_inv `(g: c ⟶ G d) `(k: d ⟶ d'): φ⁻¹ (fmap G k ◎ g) = k ◎ φ⁻¹ g.
Proof with try reflexivity; try apply _.
intros.
apply (injective φ).
rewrite surjective_applied...
rewrite φ_adjunction_natural_left...
rewrite surjective_applied...
Qed.
Let η: id ⇛ G ∘ F := λ c, φ (cat_id: F c ⟶ F c).
Let ε: F ∘ G ⇛ id := λ d, φ ⁻¹ (cat_id: G d ⟶ G d).
Global Instance η_natural: NaturalTransformation η.
Proof with try reflexivity; try apply _.
intros x' x h.
change (φ cat_id ◎ h = fmap G (fmap F h) ◎ φ cat_id).
rewrite <- φ_adjunction_natural_left, <- φ_adjunction_natural_right, left_identity, right_identity...
Qed.
Global Instance: NaturalTransformation ε.
Proof with try reflexivity; try apply _.
intros d d' f.
change ((φ ⁻¹) cat_id ◎ fmap F (fmap G f) = f ◎ (φ ⁻¹) cat_id).
rewrite
<- φ_adjunction_natural_left_inv,
<- φ_adjunction_natural_right_inv,
(left_identity (fmap G f)),
right_identity...
Qed.
Lemma φ_in_terms_of_η `(f: F x ⟶ a): φ f = fmap G f ◎ η x.
Proof.
rewrite <- (right_identity f) at 1.
rewrite φ_adjunction_natural_left. reflexivity. apply _.
Qed.
Lemma φ_in_terms_of_ε `(g: x ⟶ G a): φ⁻¹ g = ε a ◎ fmap F g.
Proof.
rewrite <- (left_identity g) at 1.
apply φ_adjunction_natural_right_inv.
Qed.
Definition univwit (c : C) (d : D): (c ⟶ G d) → (F c ⟶ d) := φ⁻¹.
Instance: ∀ c, UniversalArrow (η c: c ⟶ G (F c)) (univwit c).
Proof.
unfold univwit.
constructor; unfold compose.
rewrite <- (φ_in_terms_of_η ((φ ⁻¹) f)).
symmetry.
apply (surjective_applied _).
intros ? E.
rewrite E.
rewrite <- (φ_in_terms_of_η y).
symmetry.
apply (bijective_applied _).
Qed.
Instance φAdjunction_ηAdjunction: ηAdjunction F G η univwit := {}.
Instance φAdjunction_ηεAdjunction: ηεAdjunction F G η ε.
Proof with try apply _.
constructor; try apply _; intro x.
rewrite <- @φ_in_terms_of_η.
unfold ε. apply (surjective_applied _).
rewrite <- @φ_in_terms_of_ε.
unfold η. apply (surjective_applied _).
Qed.
(* On a side note, if we let F and G map between the duals of C and D, the adjunction is reversed: *)
Goal @φAdjunction D _ _ _ _ C _ _ _ _ G (dual.fmap_op G) F (dual.fmap_op F) (λ d c, (@φ c d)⁻¹)
(λ d c, @φ c d).
Proof with try apply _.
constructor; intros...
pose proof (φ_adjunction_bijective F G)...
change (d' ⟶ d) in k.
change (d ⟶ G c) in f.
change ((φ ⁻¹) (f ◎ k) = (φ ⁻¹) f ◎ fmap F k).
apply (injective (@φ d' c)).
rewrite (surjective_applied _).
rewrite φ_adjunction_natural_right...
now rewrite (surjective_applied _).
change (c ⟶ c') in h.
change (d ⟶ G c) in f.
change ((φ ⁻¹) (fmap G h ◎ f) = h ◎ (φ ⁻¹) f).
apply (injective (@φ d c')).
rewrite (surjective_applied _).
rewrite φ_adjunction_natural_left...
now rewrite (surjective_applied _).
Qed.
End for_φAdjunction.
Section for_ηAdjunction.
Context `(ηAdjunction).
Instance: Functor F F' := η_adjunction_left_functor F G.
Instance: Functor G G' := η_adjunction_right_functor F G.
Instance: Category D := functor_from G.
Instance: Category C := functor_to G.
Let φ x a (g: F x ⟶ a): (x ⟶ G a) := fmap G g ◎ η x.
Instance: ∀ (c: C) (d: D), Inverse (@φ c d) := uniwit.
Instance: ∀ x a, Surjective (@φ x a).
Proof with try apply _.
unfold φ.
repeat intro.
constructor.
intros x0 y E. symmetry.
rewrite <- E.
apply (η_adjunction_universal F G x).
constructor...
intros ?? E. rewrite E. reflexivity.
Qed.
Instance: ∀ x a, Injective (@φ x a).
Proof with try reflexivity; try apply _; auto.
repeat intro. constructor... unfold φ. repeat intro.
apply (equal_because_sole _ _ (η_adjunction_universal F G _ _ (fmap G x0 ◎ η x))); unfold compose...
Qed.
Instance: ∀ x a, Bijective (@φ x a) := {}.
Instance ηAdjunction_φAdjunction: φAdjunction F G φ.
Proof with try reflexivity; try apply _.
unfold φ. unfold id in *. unfold compose in η.
constructor...
repeat intro. unfold compose.
rewrite (associativity (fmap G k))...
rewrite preserves_comp...
repeat intro. unfold compose.
rewrite preserves_comp...
rewrite <- associativity.
pose proof (η_adjunction_natural F G c' c h) as P.
change (η c ◎ h = fmap G (fmap F h) ◎ η c') in P.
rewrite <- P.
rewrite (associativity (fmap G f))...
Qed.
End for_ηAdjunction.
Section for_ηεAdjunction.
Context `(ηεAdjunction).
Instance: Functor F F' := ηε_adjunction_left_functor F G.
Instance: Functor G G' := ηε_adjunction_right_functor F G.
Instance: Category D := functor_from G.
Instance: Category C := functor_to G.
Instance: NaturalTransformation η := ηε_adjunction_η_natural F G.
Instance: NaturalTransformation ε := ηε_adjunction_ε_natural F G.
Let φ c d (f: F c ⟶ d): (c ⟶ G d) := fmap G f ◎ η c.
Instance uniwit c d: Inverse (φ c d) := λ f, ε d ◎ fmap F f.
Instance ηεAdjunction_ηAdjunction: ηAdjunction F G η uniwit.
Proof with try apply _.
constructor...
unfold uniwit.
constructor; unfold compose.
rewrite preserves_comp...
pose proof (ηε_adjunction_η_natural F G c (G d) f) as P.
change (η (G d) ◎ f = fmap G (fmap F f) ◎ η c) in P.
rewrite <- associativity.
rewrite <- P.
rewrite associativity.
pose proof (ηε_adjunction_identity_at_G F G d) as Q.
simpl in Q.
rewrite Q.
symmetry.
apply left_identity.
intros y E. rewrite E. clear E f.
rewrite preserves_comp...
rewrite associativity.
pose proof (ηε_adjunction_ε_natural F G (F c) d y) as P.
change (ε d ◎ fmap F (fmap G y) = y ◎ ε (F c)) in P.
rewrite P.
rewrite <- associativity.
pose proof (ηε_adjunction_identity_at_F F G c) as Q.
simpl in Q.
rewrite Q.
symmetry.
apply right_identity.
Qed.
Instance ηεAdjunction_φAdjunction: φAdjunction F G φ.
Proof. apply ηAdjunction_φAdjunction, _. Qed.
End for_ηεAdjunction.
|
