-
Notifications
You must be signed in to change notification settings - Fork 259
/
FunctorCategory.lean
210 lines (164 loc) · 7.44 KB
/
FunctorCategory.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
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Mathlib.CategoryTheory.Monoidal.Braided.Basic
import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Functor.Const
#align_import category_theory.monoidal.functor_category from "leanprover-community/mathlib"@"73dd4b5411ec8fafb18a9d77c9c826907730af80"
/-!
# Monoidal structure on `C ⥤ D` when `D` is monoidal.
When `C` is any category, and `D` is a monoidal category,
there is a natural "pointwise" monoidal structure on `C ⥤ D`.
The initial intended application is tensor product of presheaves.
-/
universe v₁ v₂ u₁ u₂
open CategoryTheory
open CategoryTheory.MonoidalCategory
namespace CategoryTheory.Monoidal
variable {C : Type u₁} [Category.{v₁} C]
variable {D : Type u₂} [Category.{v₂} D] [MonoidalCategory.{v₂} D]
namespace FunctorCategory
variable (F G F' G' : C ⥤ D)
/-- (An auxiliary definition for `functorCategoryMonoidal`.)
Tensor product of functors `C ⥤ D`, when `D` is monoidal.
-/
@[simps]
def tensorObj : C ⥤ D where
obj X := F.obj X ⊗ G.obj X
map f := F.map f ⊗ G.map f
#align category_theory.monoidal.functor_category.tensor_obj CategoryTheory.Monoidal.FunctorCategory.tensorObj
variable {F G F' G'}
variable (α : F ⟶ G) (β : F' ⟶ G')
/-- (An auxiliary definition for `functorCategoryMonoidal`.)
Tensor product of natural transformations into `D`, when `D` is monoidal.
-/
@[simps]
def tensorHom : tensorObj F F' ⟶ tensorObj G G' where
app X := α.app X ⊗ β.app X
naturality X Y f := by dsimp; rw [← tensor_comp, α.naturality, β.naturality, tensor_comp]
#align category_theory.monoidal.functor_category.tensor_hom CategoryTheory.Monoidal.FunctorCategory.tensorHom
/-- (An auxiliary definition for `functorCategoryMonoidal`.) -/
@[simps]
def whiskerLeft (F) (β : F' ⟶ G') : tensorObj F F' ⟶ tensorObj F G' where
app X := F.obj X ◁ β.app X
naturality X Y f := by
simp only [← id_tensorHom]
apply (tensorHom (𝟙 F) β).naturality
/-- (An auxiliary definition for `functorCategoryMonoidal`.) -/
@[simps]
def whiskerRight (F') : tensorObj F F' ⟶ tensorObj G F' where
app X := α.app X ▷ F'.obj X
naturality X Y f := by
simp only [← tensorHom_id]
apply (tensorHom α (𝟙 F')).naturality
end FunctorCategory
open CategoryTheory.Monoidal.FunctorCategory
/-- When `C` is any category, and `D` is a monoidal category,
the functor category `C ⥤ D` has a natural pointwise monoidal structure,
where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
-/
instance functorCategoryMonoidalStruct : MonoidalCategoryStruct (C ⥤ D) where
tensorObj F G := tensorObj F G
tensorHom α β := tensorHom α β
whiskerLeft F _ _ α := FunctorCategory.whiskerLeft F α
whiskerRight α F := FunctorCategory.whiskerRight α F
tensorUnit := (CategoryTheory.Functor.const C).obj (𝟙_ D)
leftUnitor F := NatIso.ofComponents fun X => λ_ (F.obj X)
rightUnitor F := NatIso.ofComponents fun X => ρ_ (F.obj X)
associator F G H := NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)
@[simp]
theorem tensorUnit_obj {X} : (𝟙_ (C ⥤ D)).obj X = 𝟙_ D :=
rfl
#align category_theory.monoidal.tensor_unit_obj CategoryTheory.Monoidal.tensorUnit_obj
@[simp]
theorem tensorUnit_map {X Y} {f : X ⟶ Y} : (𝟙_ (C ⥤ D)).map f = 𝟙 (𝟙_ D) :=
rfl
#align category_theory.monoidal.tensor_unit_map CategoryTheory.Monoidal.tensorUnit_map
@[simp]
theorem tensorObj_obj {F G : C ⥤ D} {X} : (F ⊗ G).obj X = F.obj X ⊗ G.obj X :=
rfl
#align category_theory.monoidal.tensor_obj_obj CategoryTheory.Monoidal.tensorObj_obj
@[simp]
theorem tensorObj_map {F G : C ⥤ D} {X Y} {f : X ⟶ Y} : (F ⊗ G).map f = F.map f ⊗ G.map f :=
rfl
#align category_theory.monoidal.tensor_obj_map CategoryTheory.Monoidal.tensorObj_map
@[simp]
theorem tensorHom_app {F G F' G' : C ⥤ D} {α : F ⟶ G} {β : F' ⟶ G'} {X} :
(α ⊗ β).app X = α.app X ⊗ β.app X :=
rfl
#align category_theory.monoidal.tensor_hom_app CategoryTheory.Monoidal.tensorHom_app
@[simp]
theorem whiskerLeft_app {F F' G' : C ⥤ D} {β : F' ⟶ G'} {X} :
(F ◁ β).app X = F.obj X ◁ β.app X :=
rfl
@[simp]
theorem whiskerRight_app {F G F' : C ⥤ D} {α : F ⟶ G} {X} :
(α ▷ F').app X = α.app X ▷ F'.obj X :=
rfl
@[simp]
theorem leftUnitor_hom_app {F : C ⥤ D} {X} :
((λ_ F).hom : 𝟙_ _ ⊗ F ⟶ F).app X = (λ_ (F.obj X)).hom :=
rfl
#align category_theory.monoidal.left_unitor_hom_app CategoryTheory.Monoidal.leftUnitor_hom_app
@[simp]
theorem leftUnitor_inv_app {F : C ⥤ D} {X} :
((λ_ F).inv : F ⟶ 𝟙_ _ ⊗ F).app X = (λ_ (F.obj X)).inv :=
rfl
#align category_theory.monoidal.left_unitor_inv_app CategoryTheory.Monoidal.leftUnitor_inv_app
@[simp]
theorem rightUnitor_hom_app {F : C ⥤ D} {X} :
((ρ_ F).hom : F ⊗ 𝟙_ _ ⟶ F).app X = (ρ_ (F.obj X)).hom :=
rfl
#align category_theory.monoidal.right_unitor_hom_app CategoryTheory.Monoidal.rightUnitor_hom_app
@[simp]
theorem rightUnitor_inv_app {F : C ⥤ D} {X} :
((ρ_ F).inv : F ⟶ F ⊗ 𝟙_ _).app X = (ρ_ (F.obj X)).inv :=
rfl
#align category_theory.monoidal.right_unitor_inv_app CategoryTheory.Monoidal.rightUnitor_inv_app
@[simp]
theorem associator_hom_app {F G H : C ⥤ D} {X} :
((α_ F G H).hom : (F ⊗ G) ⊗ H ⟶ F ⊗ G ⊗ H).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).hom :=
rfl
#align category_theory.monoidal.associator_hom_app CategoryTheory.Monoidal.associator_hom_app
@[simp]
theorem associator_inv_app {F G H : C ⥤ D} {X} :
((α_ F G H).inv : F ⊗ G ⊗ H ⟶ (F ⊗ G) ⊗ H).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).inv :=
rfl
#align category_theory.monoidal.associator_inv_app CategoryTheory.Monoidal.associator_inv_app
/-- When `C` is any category, and `D` is a monoidal category,
the functor category `C ⥤ D` has a natural pointwise monoidal structure,
where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
-/
instance functorCategoryMonoidal : MonoidalCategory (C ⥤ D) where
tensorHom_def := by intros; ext; simp [tensorHom_def]
pentagon F G H K := by ext X; dsimp; rw [pentagon]
#align category_theory.monoidal.functor_category_monoidal CategoryTheory.Monoidal.functorCategoryMonoidal
section BraidedCategory
open CategoryTheory.BraidedCategory
variable [BraidedCategory.{v₂} D]
/-- When `C` is any category, and `D` is a braided monoidal category,
the natural pointwise monoidal structure on the functor category `C ⥤ D`
is also braided.
-/
instance functorCategoryBraided : BraidedCategory (C ⥤ D) where
braiding F G := NatIso.ofComponents fun X => β_ _ _
hexagon_forward F G H := by ext X; apply hexagon_forward
hexagon_reverse F G H := by ext X; apply hexagon_reverse
#align category_theory.monoidal.functor_category_braided CategoryTheory.Monoidal.functorCategoryBraided
example : BraidedCategory (C ⥤ D) :=
CategoryTheory.Monoidal.functorCategoryBraided
end BraidedCategory
section SymmetricCategory
open CategoryTheory.SymmetricCategory
variable [SymmetricCategory.{v₂} D]
/-- When `C` is any category, and `D` is a symmetric monoidal category,
the natural pointwise monoidal structure on the functor category `C ⥤ D`
is also symmetric.
-/
instance functorCategorySymmetric : SymmetricCategory (C ⥤ D) where
symmetry F G := by ext X; apply symmetry
#align category_theory.monoidal.functor_category_symmetric CategoryTheory.Monoidal.functorCategorySymmetric
end SymmetricCategory
end CategoryTheory.Monoidal