-
Notifications
You must be signed in to change notification settings - Fork 297
/
End.lean
307 lines (267 loc) · 10.5 KB
/
End.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
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Andrew Yang
-/
import category_theory.monoidal.functor
/-!
# Endofunctors as a monoidal category.
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
We give the monoidal category structure on `C ⥤ C`,
and show that when `C` itself is monoidal, it embeds via a monoidal functor into `C ⥤ C`.
## TODO
Can we use this to show coherence results, e.g. a cheap proof that `λ_ (𝟙_ C) = ρ_ (𝟙_ C)`?
I suspect this is harder than is usually made out.
-/
universes v u
namespace category_theory
variables (C : Type u) [category.{v} C]
/--
The category of endofunctors of any category is a monoidal category,
with tensor product given by composition of functors
(and horizontal composition of natural transformations).
-/
def endofunctor_monoidal_category : monoidal_category (C ⥤ C) :=
{ tensor_obj := λ F G, F ⋙ G,
tensor_hom := λ F G F' G' α β, α ◫ β,
tensor_unit := 𝟭 C,
associator := λ F G H, functor.associator F G H,
left_unitor := λ F, functor.left_unitor F,
right_unitor := λ F, functor.right_unitor F, }.
open category_theory.monoidal_category
local attribute [instance] endofunctor_monoidal_category
local attribute [reducible] endofunctor_monoidal_category
/--
Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
-/
@[simps]
def tensoring_right_monoidal [monoidal_category.{v} C] : monoidal_functor C (C ⥤ C) :=
{ ε := (right_unitor_nat_iso C).inv,
μ := λ X Y,
{ app := λ Z, (α_ Z X Y).hom,
naturality' := λ Z Z' f, by { dsimp, rw associator_naturality, simp, } },
μ_natural' := λ X Y X' Y' f g, by { ext Z, dsimp,
simp only [←id_tensor_comp_tensor_id g f, id_tensor_comp, ←tensor_id, category.assoc,
associator_naturality, associator_naturality_assoc], },
associativity' := λ X Y Z, by { ext W, dsimp, simp [pentagon], },
left_unitality' := λ X, by { ext Y, dsimp, rw [category.id_comp, triangle, ←tensor_comp], simp, },
right_unitality' := λ X,
begin
ext Y, dsimp,
rw [tensor_id, category.comp_id, right_unitor_tensor_inv, category.assoc, iso.inv_hom_id_assoc,
←id_tensor_comp, iso.inv_hom_id, tensor_id],
end,
ε_is_iso := by apply_instance,
μ_is_iso := λ X Y,
-- We could avoid needing to do this explicitly by
-- constructing a partially applied analogue of `associator_nat_iso`.
⟨⟨{ app := λ Z, (α_ Z X Y).inv,
naturality' := λ Z Z' f, by { dsimp, rw ←associator_inv_naturality, simp, } },
by tidy⟩⟩,
..tensoring_right C }.
variable {C}
variables {M : Type*} [category M] [monoidal_category M] (F : monoidal_functor M (C ⥤ C))
@[simp, reassoc]
lemma μ_hom_inv_app (i j : M) (X : C) :
(F.μ i j).app X ≫ (F.μ_iso i j).inv.app X = 𝟙 _ := (F.μ_iso i j).hom_inv_id_app X
@[simp, reassoc]
lemma μ_inv_hom_app (i j : M) (X : C) :
(F.μ_iso i j).inv.app X ≫ (F.μ i j).app X = 𝟙 _ := (F.μ_iso i j).inv_hom_id_app X
@[simp, reassoc]
lemma ε_hom_inv_app (X : C) :
F.ε.app X ≫ F.ε_iso.inv.app X = 𝟙 _ := F.ε_iso.hom_inv_id_app X
@[simp, reassoc]
lemma ε_inv_hom_app (X : C) :
F.ε_iso.inv.app X ≫ F.ε.app X = 𝟙 _ := F.ε_iso.inv_hom_id_app X
@[simp, reassoc]
lemma ε_naturality {X Y : C} (f : X ⟶ Y) :
F.ε.app X ≫ (F.obj (𝟙_M)).map f = f ≫ F.ε.app Y := (F.ε.naturality f).symm
@[simp, reassoc]
lemma ε_inv_naturality {X Y : C} (f : X ⟶ Y) :
(F.obj (𝟙_M)).map f ≫ F.ε_iso.inv.app Y = F.ε_iso.inv.app X ≫ f :=
F.ε_iso.inv.naturality f
@[simp, reassoc]
lemma μ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
(F.obj n).map ((F.obj m).map f) ≫ (F.μ m n).app Y = (F.μ m n).app X ≫ (F.obj _).map f :=
(F.to_lax_monoidal_functor.μ m n).naturality f
-- This is a simp lemma in the reverse direction via `nat_trans.naturality`.
@[reassoc]
lemma μ_inv_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
(F.μ_iso m n).inv.app X ≫ (F.obj n).map ((F.obj m).map f) =
(F.obj _).map f ≫ (F.μ_iso m n).inv.app Y :=
((F.μ_iso m n).inv.naturality f).symm
-- This is not a simp lemma since it could be proved by the lemmas later.
@[reassoc]
lemma μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) :
(F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (F.μ m' n').app X =
(F.μ m n).app X ≫ (F.map (f ⊗ g)).app X :=
begin
have := congr_app (F.to_lax_monoidal_functor.μ_natural f g) X,
dsimp at this,
simpa using this,
end
@[simp, reassoc]
lemma μ_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
(F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X =
(F.μ m n).app X ≫ (F.map (f ⊗ 𝟙 n)).app X :=
begin
rw ← μ_naturality₂ F f (𝟙 n) X,
simp,
end
@[simp, reassoc]
lemma μ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
(F.map g).app ((F.obj m).obj X) ≫ (F.μ m n').app X =
(F.μ m n).app X ≫ (F.map (𝟙 m ⊗ g)).app X :=
begin
rw ← μ_naturality₂ F (𝟙 m) g X,
simp,
end
@[simp, reassoc]
lemma μ_inv_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
(F.μ_iso m n).inv.app X ≫ (F.obj n).map ((F.map f).app X) =
(F.map (f ⊗ 𝟙 n)).app X ≫ (F.μ_iso m' n).inv.app X :=
begin
rw [← is_iso.comp_inv_eq, category.assoc, ← is_iso.eq_inv_comp],
simp,
end
@[simp, reassoc]
lemma μ_inv_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
(F.μ_iso m n).inv.app X ≫ (F.map g).app ((F.obj m).obj X) =
(F.map (𝟙 m ⊗ g)).app X ≫ (F.μ_iso m n').inv.app X :=
begin
rw [← is_iso.comp_inv_eq, category.assoc, ← is_iso.eq_inv_comp],
simp,
end
@[reassoc]
lemma left_unitality_app (n : M) (X : C) :
(F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_M) n).app X
≫ (F.map (λ_ n).hom).app X = 𝟙 _ :=
begin
have := congr_app (F.to_lax_monoidal_functor.left_unitality n) X,
dsimp at this,
simpa using this.symm,
end
@[reassoc, simp]
lemma obj_ε_app (n : M) (X : C) :
(F.obj n).map (F.ε.app X) =
(F.map (λ_ n).inv).app X ≫ (F.μ_iso (𝟙_M) n).inv.app X :=
begin
refine eq.trans _ (category.id_comp _),
rw [← category.assoc, ← is_iso.comp_inv_eq, ← is_iso.comp_inv_eq, category.assoc],
convert left_unitality_app F n X,
{ simp },
{ ext, simpa }
end
@[reassoc, simp]
lemma obj_ε_inv_app (n : M) (X : C) :
(F.obj n).map (F.ε_iso.inv.app X) =
(F.μ (𝟙_M) n).app X ≫ (F.map (λ_ n).hom).app X :=
begin
rw [← cancel_mono ((F.obj n).map (F.ε.app X)), ← functor.map_comp],
simpa,
end
@[reassoc]
lemma right_unitality_app (n : M) (X : C) :
F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 _ :=
begin
have := congr_app (F.to_lax_monoidal_functor.right_unitality n) X,
dsimp at this,
simpa using this.symm,
end
@[simp]
lemma ε_app_obj (n : M) (X : C) :
F.ε.app ((F.obj n).obj X) =
(F.map (ρ_ n).inv).app X ≫ (F.μ_iso n (𝟙_M)).inv.app X :=
begin
refine eq.trans _ (category.id_comp _),
rw [← category.assoc, ← is_iso.comp_inv_eq, ← is_iso.comp_inv_eq, category.assoc],
convert right_unitality_app F n X,
{ simp },
{ ext, simpa }
end
@[simp]
lemma ε_inv_app_obj (n : M) (X : C) :
F.ε_iso.inv.app ((F.obj n).obj X) =
(F.μ n (𝟙_M)).app X ≫ (F.map (ρ_ n).hom).app X :=
begin
rw [← cancel_mono (F.ε.app ((F.obj n).obj X)), ε_inv_hom_app],
simpa
end
@[reassoc]
lemma associativity_app (m₁ m₂ m₃: M) (X : C) :
(F.obj m₃).map ((F.μ m₁ m₂).app X) ≫ (F.μ (m₁ ⊗ m₂) m₃).app X ≫
(F.map (α_ m₁ m₂ m₃).hom).app X =
(F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X :=
begin
have := congr_app (F.to_lax_monoidal_functor.associativity m₁ m₂ m₃) X,
dsimp at this,
simpa using this,
end
@[reassoc, simp]
lemma obj_μ_app (m₁ m₂ m₃ : M) (X : C) :
(F.obj m₃).map ((F.μ m₁ m₂).app X) =
(F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X ≫
(F.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μ_iso (m₁ ⊗ m₂) m₃).inv.app X :=
begin
rw [← associativity_app_assoc],
dsimp,
simp,
dsimp,
simp,
end
@[reassoc, simp]
lemma obj_μ_inv_app (m₁ m₂ m₃ : M) (X : C) :
(F.obj m₃).map ((F.μ_iso m₁ m₂).inv.app X) =
(F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X ≫
(F.μ_iso m₁ (m₂ ⊗ m₃)).inv.app X ≫
(F.μ_iso m₂ m₃).inv.app ((F.obj m₁).obj X) :=
begin
rw ← is_iso.inv_eq_inv,
convert obj_μ_app F m₁ m₂ m₃ X using 1,
{ ext, rw ← functor.map_comp, simp },
{ simp only [monoidal_functor.μ_iso_hom, category.assoc, nat_iso.inv_inv_app, is_iso.inv_comp],
congr,
{ ext, simp },
{ ext, simpa } }
end
@[simp, reassoc]
lemma obj_zero_map_μ_app {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) :
(F.obj (𝟙_M)).map f ≫ (F.μ m (𝟙_M)).app _ =
F.ε_iso.inv.app _ ≫ f ≫ (F.map (ρ_ m).inv).app _ :=
begin
rw [← is_iso.inv_comp_eq, ← is_iso.comp_inv_eq],
simp,
end
@[simp]
lemma obj_μ_zero_app (m₁ m₂ : M) (X : C) :
(F.obj m₂).map ((F.μ m₁ (𝟙_M)).app X) =
(F.μ (𝟙_M) m₂).app ((F.obj m₁).obj X) ≫ (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫
(F.obj m₂).map ((F.map (ρ_ m₁).inv).app X) :=
begin
rw [← obj_ε_inv_app_assoc, ← functor.map_comp],
congr, simp,
end
/-- If `m ⊗ n ≅ 𝟙_M`, then `F.obj m` is a left inverse of `F.obj n`. -/
@[simps] noncomputable
def unit_of_tensor_iso_unit (m n : M) (h : m ⊗ n ≅ 𝟙_M) : F.obj m ⋙ F.obj n ≅ 𝟭 C :=
F.μ_iso m n ≪≫ F.to_functor.map_iso h ≪≫ F.ε_iso.symm
/-- If `m ⊗ n ≅ 𝟙_M` and `n ⊗ m ≅ 𝟙_M` (subject to some commuting constraints),
then `F.obj m` and `F.obj n` forms a self-equivalence of `C`. -/
@[simps] noncomputable
def equiv_of_tensor_iso_unit (m n : M) (h₁ : m ⊗ n ≅ 𝟙_M) (h₂ : n ⊗ m ≅ 𝟙_M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) : C ≌ C :=
{ functor := F.obj m,
inverse := F.obj n,
unit_iso := (unit_of_tensor_iso_unit F m n h₁).symm,
counit_iso := unit_of_tensor_iso_unit F n m h₂,
functor_unit_iso_comp' :=
begin
intro X,
dsimp,
simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, ε_inv_app_obj, category.assoc,
obj_μ_inv_app, functor.map_comp, μ_inv_hom_app_assoc, obj_ε_app,
unit_of_tensor_iso_unit_inv_app],
simp [← nat_trans.comp_app, ← F.to_functor.map_comp, ← H, - functor.map_comp]
end }
end category_theory