-
Notifications
You must be signed in to change notification settings - Fork 307
/
Whiskering.lean
291 lines (237 loc) · 11.8 KB
/
Whiskering.lean
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
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Functor.FullyFaithful
#align_import category_theory.whiskering from "leanprover-community/mathlib"@"d012cd09a9b256d870751284dd6a29882b0be105"
/-!
# Whiskering
Given a functor `F : C ⥤ D` and functors `G H : D ⥤ E` and a natural transformation `α : G ⟶ H`,
we can construct a new natural transformation `F ⋙ G ⟶ F ⋙ H`,
called `whiskerLeft F α`. This is the same as the horizontal composition of `𝟙 F` with `α`.
This operation is functorial in `F`, and we package this as `whiskeringLeft`. Here
`(whiskeringLeft.obj F).obj G` is `F ⋙ G`, and
`(whiskeringLeft.obj F).map α` is `whiskerLeft F α`.
(That is, we might have alternatively named this as the "left composition functor".)
We also provide analogues for composition on the right, and for these operations on isomorphisms.
At the end of the file, we provide the left and right unitors, and the associator,
for functor composition.
(In fact functor composition is definitionally associative, but very often relying on this causes
extremely slow elaboration, so it is better to insert it explicitly.)
We also show these natural isomorphisms satisfy the triangle and pentagon identities.
-/
namespace CategoryTheory
universe u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄
section
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {E : Type u₃}
[Category.{v₃} E]
/-- If `α : G ⟶ H` then
`whiskerLeft F α : (F ⋙ G) ⟶ (F ⋙ H)` has components `α.app (F.obj X)`.
-/
@[simps]
def whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) :
F ⋙ G ⟶ F ⋙ H where
app X := α.app (F.obj X)
naturality X Y f := by rw [Functor.comp_map, Functor.comp_map, α.naturality]
#align category_theory.whisker_left CategoryTheory.whiskerLeft
#align category_theory.whisker_left_app CategoryTheory.whiskerLeft_app
/-- If `α : G ⟶ H` then
`whisker_right α F : (G ⋙ F) ⟶ (G ⋙ F)` has components `F.map (α.app X)`.
-/
@[simps]
def whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) :
G ⋙ F ⟶ H ⋙ F where
app X := F.map (α.app X)
naturality X Y f := by
rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
#align category_theory.whisker_right CategoryTheory.whiskerRight
#align category_theory.whisker_right_app CategoryTheory.whiskerRight_app
variable (C D E)
/-- Left-composition gives a functor `(C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E))`.
`(whiskeringLeft.obj F).obj G` is `F ⋙ G`, and
`(whiskeringLeft.obj F).map α` is `whiskerLeft F α`.
-/
@[simps]
def whiskeringLeft : (C ⥤ D) ⥤ (D ⥤ E) ⥤ C ⥤ E where
obj F :=
{ obj := fun G => F ⋙ G
map := fun α => whiskerLeft F α }
map τ :=
{ app := fun H =>
{ app := fun c => H.map (τ.app c)
naturality := fun X Y f => by dsimp; rw [← H.map_comp, ← H.map_comp, ← τ.naturality] }
naturality := fun X Y f => by ext; dsimp; rw [f.naturality] }
#align category_theory.whiskering_left CategoryTheory.whiskeringLeft
#align category_theory.whiskering_left_obj_map CategoryTheory.whiskeringLeft_obj_map
#align category_theory.whiskering_left_obj_obj CategoryTheory.whiskeringLeft_obj_obj
#align category_theory.whiskering_left_map_app_app CategoryTheory.whiskeringLeft_map_app_app
/-- Right-composition gives a functor `(D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))`.
`(whiskeringRight.obj H).obj F` is `F ⋙ H`, and
`(whiskeringRight.obj H).map α` is `whiskerRight α H`.
-/
@[simps]
def whiskeringRight : (D ⥤ E) ⥤ (C ⥤ D) ⥤ C ⥤ E where
obj H :=
{ obj := fun F => F ⋙ H
map := fun α => whiskerRight α H }
map τ :=
{ app := fun F =>
{ app := fun c => τ.app (F.obj c)
naturality := fun X Y f => by dsimp; rw [τ.naturality] }
naturality := fun X Y f => by ext; dsimp; rw [← NatTrans.naturality] }
#align category_theory.whiskering_right CategoryTheory.whiskeringRight
#align category_theory.whiskering_right_map_app_app CategoryTheory.whiskeringRight_map_app_app
#align category_theory.whiskering_right_obj_obj CategoryTheory.whiskeringRight_obj_obj
#align category_theory.whiskering_right_obj_map CategoryTheory.whiskeringRight_obj_map
variable {C} {D} {E}
instance faithful_whiskeringRight_obj {F : D ⥤ E} [Faithful F] :
Faithful ((whiskeringRight C D E).obj F) where
map_injective hαβ := by
ext X
exact (F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X)
#align category_theory.faithful_whiskering_right_obj CategoryTheory.faithful_whiskeringRight_obj
@[simp]
theorem whiskerLeft_id (F : C ⥤ D) {G : D ⥤ E} :
whiskerLeft F (NatTrans.id G) = NatTrans.id (F.comp G) :=
rfl
#align category_theory.whisker_left_id CategoryTheory.whiskerLeft_id
@[simp]
theorem whiskerLeft_id' (F : C ⥤ D) {G : D ⥤ E} : whiskerLeft F (𝟙 G) = 𝟙 (F.comp G) :=
rfl
#align category_theory.whisker_left_id' CategoryTheory.whiskerLeft_id'
@[simp]
theorem whiskerRight_id {G : C ⥤ D} (F : D ⥤ E) :
whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F) :=
((whiskeringRight C D E).obj F).map_id _
#align category_theory.whisker_right_id CategoryTheory.whiskerRight_id
@[simp]
theorem whiskerRight_id' {G : C ⥤ D} (F : D ⥤ E) : whiskerRight (𝟙 G) F = 𝟙 (G.comp F) :=
((whiskeringRight C D E).obj F).map_id _
#align category_theory.whisker_right_id' CategoryTheory.whiskerRight_id'
@[simp, reassoc]
theorem whiskerLeft_comp (F : C ⥤ D) {G H K : D ⥤ E} (α : G ⟶ H) (β : H ⟶ K) :
whiskerLeft F (α ≫ β) = whiskerLeft F α ≫ whiskerLeft F β :=
rfl
#align category_theory.whisker_left_comp CategoryTheory.whiskerLeft_comp
@[simp, reassoc]
theorem whiskerRight_comp {G H K : C ⥤ D} (α : G ⟶ H) (β : H ⟶ K) (F : D ⥤ E) :
whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F :=
((whiskeringRight C D E).obj F).map_comp α β
#align category_theory.whisker_right_comp CategoryTheory.whiskerRight_comp
/-- If `α : G ≅ H` is a natural isomorphism then
`iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H)` has components `α.app (F.obj X)`.
-/
def isoWhiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : F ⋙ G ≅ F ⋙ H :=
((whiskeringLeft C D E).obj F).mapIso α
#align category_theory.iso_whisker_left CategoryTheory.isoWhiskerLeft
@[simp]
theorem isoWhiskerLeft_hom (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
(isoWhiskerLeft F α).hom = whiskerLeft F α.hom :=
rfl
#align category_theory.iso_whisker_left_hom CategoryTheory.isoWhiskerLeft_hom
@[simp]
theorem isoWhiskerLeft_inv (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
(isoWhiskerLeft F α).inv = whiskerLeft F α.inv :=
rfl
#align category_theory.iso_whisker_left_inv CategoryTheory.isoWhiskerLeft_inv
/-- If `α : G ≅ H` then
`iso_whisker_right α F : (G ⋙ F) ≅ (H ⋙ F)` has components `F.map_iso (α.app X)`.
-/
def isoWhiskerRight {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : G ⋙ F ≅ H ⋙ F :=
((whiskeringRight C D E).obj F).mapIso α
#align category_theory.iso_whisker_right CategoryTheory.isoWhiskerRight
@[simp]
theorem isoWhiskerRight_hom {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
(isoWhiskerRight α F).hom = whiskerRight α.hom F :=
rfl
#align category_theory.iso_whisker_right_hom CategoryTheory.isoWhiskerRight_hom
@[simp]
theorem isoWhiskerRight_inv {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
(isoWhiskerRight α F).inv = whiskerRight α.inv F :=
rfl
#align category_theory.iso_whisker_right_inv CategoryTheory.isoWhiskerRight_inv
instance isIso_whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [IsIso α] :
IsIso (whiskerLeft F α) :=
IsIso.of_iso (isoWhiskerLeft F (asIso α))
#align category_theory.is_iso_whisker_left CategoryTheory.isIso_whiskerLeft
instance isIso_whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [IsIso α] :
IsIso (whiskerRight α F) :=
IsIso.of_iso (isoWhiskerRight (asIso α) F)
#align category_theory.is_iso_whisker_right CategoryTheory.isIso_whiskerRight
variable {B : Type u₄} [Category.{v₄} B]
-- Porting note: it was `attribute [local elab_without_expected_type]`,
-- but now `elab_without_expected-type` must be global
attribute [elab_without_expected_type] whiskerLeft whiskerRight
@[simp]
theorem whiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) :
whiskerLeft F (whiskerLeft G α) = whiskerLeft (F ⋙ G) α :=
rfl
#align category_theory.whisker_left_twice CategoryTheory.whiskerLeft_twice
@[simp]
theorem whiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) :
whiskerRight (whiskerRight α F) G = whiskerRight α (F ⋙ G) :=
rfl
#align category_theory.whisker_right_twice CategoryTheory.whiskerRight_twice
theorem whiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) :
whiskerRight (whiskerLeft F α) K = whiskerLeft F (whiskerRight α K) :=
rfl
#align category_theory.whisker_right_left CategoryTheory.whiskerRight_left
end
namespace Functor
universe u₅ v₅
variable {A : Type u₁} [Category.{v₁} A]
variable {B : Type u₂} [Category.{v₂} B]
/-- The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
-/
@[simps]
def leftUnitor (F : A ⥤ B) :
𝟭 A ⋙ F ≅ F where
hom := { app := fun X => 𝟙 (F.obj X) }
inv := { app := fun X => 𝟙 (F.obj X) }
#align category_theory.functor.left_unitor CategoryTheory.Functor.leftUnitor
#align category_theory.functor.left_unitor_inv_app CategoryTheory.Functor.leftUnitor_inv_app
#align category_theory.functor.left_unitor_hom_app CategoryTheory.Functor.leftUnitor_hom_app
/-- The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
-/
@[simps]
def rightUnitor (F : A ⥤ B) :
F ⋙ 𝟭 B ≅ F where
hom := { app := fun X => 𝟙 (F.obj X) }
inv := { app := fun X => 𝟙 (F.obj X) }
#align category_theory.functor.right_unitor CategoryTheory.Functor.rightUnitor
#align category_theory.functor.right_unitor_hom_app CategoryTheory.Functor.rightUnitor_hom_app
#align category_theory.functor.right_unitor_inv_app CategoryTheory.Functor.rightUnitor_inv_app
variable {C : Type u₃} [Category.{v₃} C]
variable {D : Type u₄} [Category.{v₄} D]
/-- The associator for functors, a natural isomorphism `((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H))`.
(In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
and it's usually best to insert explicit associators.)
-/
@[simps]
def associator (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) :
(F ⋙ G) ⋙ H ≅ F ⋙ G ⋙ H where
hom := { app := fun _ => 𝟙 _ }
inv := { app := fun _ => 𝟙 _ }
#align category_theory.functor.associator CategoryTheory.Functor.associator
#align category_theory.functor.associator_inv_app CategoryTheory.Functor.associator_inv_app
#align category_theory.functor.associator_hom_app CategoryTheory.Functor.associator_hom_app
protected theorem assoc (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) : (F ⋙ G) ⋙ H = F ⋙ G ⋙ H :=
rfl
#align category_theory.functor.assoc CategoryTheory.Functor.assoc
theorem triangle (F : A ⥤ B) (G : B ⥤ C) :
(associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom =
whiskerRight (rightUnitor F).hom G := by aesop_cat
#align category_theory.functor.triangle CategoryTheory.Functor.triangle
-- See note [dsimp, simp].
variable {E : Type u₅} [Category.{v₅} E]
variable (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) (K : D ⥤ E)
theorem pentagon :
whiskerRight (associator F G H).hom K ≫
(associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
(associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom := by aesop_cat
#align category_theory.functor.pentagon CategoryTheory.Functor.pentagon
end Functor
end CategoryTheory