Skip to content

Commit 47acb74

Browse files
joelrioujoelriou
committed
feat(CategoryTheory): the monoidal category structure on a localization (#20951)
In #12728, we shall show that if `C` is a monoidal category and `W` is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the `MonoidalCategoryStruct` instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
1 parent ac2479c commit 47acb74

File tree

3 files changed

+292
-2
lines changed

3 files changed

+292
-2
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2052,6 +2052,7 @@ import Mathlib.CategoryTheory.Localization.HasLocalization
20522052
import Mathlib.CategoryTheory.Localization.HomEquiv
20532053
import Mathlib.CategoryTheory.Localization.LocalizerMorphism
20542054
import Mathlib.CategoryTheory.Localization.LocallySmall
2055+
import Mathlib.CategoryTheory.Localization.Monoidal
20552056
import Mathlib.CategoryTheory.Localization.Opposite
20562057
import Mathlib.CategoryTheory.Localization.Pi
20572058
import Mathlib.CategoryTheory.Localization.Predicate

‎Mathlib/CategoryTheory/Localization/Monoidal.lean‎

Lines changed: 282 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,282 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou, Dagur Asgeirsson
5+
-/
6+
import Mathlib.CategoryTheory.Localization.Trifunctor
7+
import Mathlib.CategoryTheory.Monoidal.Category
8+
9+
/-!
10+
# Localization of monoidal categories
11+
12+
Let `C` be a monoidal category equipped with a class of morphisms `W` which
13+
is compatible with the monoidal category structure: this means `W`
14+
is multiplicative and stable by left and right whiskerings (this is
15+
the type class `W.IsMonoidal`). Let `L : C ⥤ D` be a localization functor
16+
for `W`. In the file, we shall construct a monoidal category structure
17+
on `D` such that the localization functor is monoidal. The structure
18+
is actually defined on a type synonym `LocalizedMonoidal L W ε`.
19+
Here, the data `ε : L.obj (𝟙_ C) ≅ unit` is an isomorphism to some
20+
object `unit : D` which allows the user to provide a preferred choice
21+
of a unit object.
22+
23+
-/
24+
25+
namespace CategoryTheory
26+
27+
open Category MonoidalCategory
28+
29+
variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) (W : MorphismProperty C)
30+
[MonoidalCategory C]
31+
32+
namespace MorphismProperty
33+
34+
/-- A class of morphisms `W` in a monoidal category is monoidal if it is multiplicative
35+
and stable under left and right whiskering. Under this condition, the localized
36+
category can be equipped with a monoidal category structure, see `LocalizedMonoidal`. -/
37+
class IsMonoidal extends W.IsMultiplicative : Prop where
38+
whiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (X ◁ g)
39+
whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : W f) (Y : C) : W (f ▷ Y)
40+
41+
variable [W.IsMonoidal]
42+
43+
lemma whiskerLeft_mem (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (X ◁ g) :=
44+
IsMonoidal.whiskerLeft _ _ hg
45+
46+
lemma whiskerRight_mem {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : W f) (Y : C) : W (f ▷ Y) :=
47+
IsMonoidal.whiskerRight _ hf Y
48+
49+
lemma tensorHom_mem {X₁ X₂ : C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂)
50+
(hf : W f) (hg : W g) : W (f ⊗ g) := by
51+
rw [tensorHom_def]
52+
exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)
53+
54+
end MorphismProperty
55+
56+
/-- Given a monoidal category `C`, a localization functor `L : C ⥤ D` with respect
57+
to `W : MorphismProperty C` which satisfies `W.IsMonoidal`, and a choice
58+
of object `unit : D` with an isomorphism `L.obj (𝟙_ C) ≅ unit`, this is a
59+
type synonym for `D` on which we define the localized monoidal category structure. -/
60+
@[nolint unusedArguments]
61+
def LocalizedMonoidal (L : C ⥤ D) (W : MorphismProperty C)
62+
[W.IsMonoidal] [L.IsLocalization W] {unit : D} (_ : L.obj (𝟙_ C) ≅ unit) :=
63+
D
64+
65+
variable [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (𝟙_ C) ≅ unit)
66+
67+
namespace Localization
68+
69+
instance : Category (LocalizedMonoidal L W ε) :=
70+
inferInstanceAs (Category D)
71+
72+
namespace Monoidal
73+
74+
/-- The monoidal functor from a monoidal category `C` to
75+
its localization `LocalizedMonoidal L W ε`. -/
76+
def toMonoidalCategory : C ⥤ LocalizedMonoidal L W ε := L
77+
78+
/-- The isomorphism `ε : L.obj (𝟙_ C) ≅ unit`,
79+
as `(toMonoidalCategory L W ε).obj (𝟙_ C) ≅ unit`. -/
80+
abbrev ε' : (toMonoidalCategory L W ε).obj (𝟙_ C) ≅ unit := ε
81+
82+
local notation "L'" => toMonoidalCategory L W ε
83+
84+
instance : (L').IsLocalization W := inferInstanceAs (L.IsLocalization W)
85+
86+
lemma isInvertedBy₂ :
87+
MorphismProperty.IsInvertedBy₂ W W
88+
(curriedTensor C ⋙ (whiskeringRight C C D).obj L') := by
89+
rintro ⟨X₁, Y₁⟩ ⟨X₂, Y₂⟩ ⟨f₁, f₂⟩ ⟨hf₁, hf₂⟩
90+
have := Localization.inverts L' W _ (W.whiskerRight_mem f₁ hf₁ Y₁)
91+
have := Localization.inverts L' W _ (W.whiskerLeft_mem X₂ f₂ hf₂)
92+
dsimp
93+
infer_instance
94+
95+
/-- The localized tensor product, as a bifunctor. -/
96+
noncomputable def tensorBifunctor :
97+
LocalizedMonoidal L W ε ⥤ LocalizedMonoidal L W ε ⥤ LocalizedMonoidal L W ε :=
98+
Localization.lift₂ _ (isInvertedBy₂ L W ε) L L
99+
100+
noncomputable instance : Lifting₂ L' L' W W (curriedTensor C ⋙ (whiskeringRight C C
101+
(LocalizedMonoidal L W ε)).obj L') (tensorBifunctor L W ε) :=
102+
inferInstanceAs (Lifting₂ L L W W (curriedTensor C ⋙ (whiskeringRight C C D).obj L')
103+
(Localization.lift₂ _ (isInvertedBy₂ L W ε) L L))
104+
105+
/-- The bifunctor `tensorBifunctor` on `LocalizedMonoidal L W ε` is induced by
106+
`curriedTensor C`. -/
107+
noncomputable abbrev tensorBifunctorIso :
108+
(((whiskeringLeft₂ D).obj L').obj L').obj (tensorBifunctor L W ε) ≅
109+
(Functor.postcompose₂.obj L').obj (curriedTensor C) :=
110+
Lifting₂.iso L' L' W W (curriedTensor C ⋙ (whiskeringRight C C
111+
(LocalizedMonoidal L W ε)).obj L') (tensorBifunctor L W ε)
112+
113+
noncomputable instance (X : C) :
114+
Lifting L' W (tensorLeft X ⋙ L') ((tensorBifunctor L W ε).obj ((L').obj X)) := by
115+
apply Lifting₂.liftingLift₂ (hF := isInvertedBy₂ L W ε)
116+
117+
noncomputable instance (Y : C) :
118+
Lifting L' W (tensorRight Y ⋙ L') ((tensorBifunctor L W ε).flip.obj ((L').obj Y)) := by
119+
apply Lifting₂.liftingLift₂Flip (hF := isInvertedBy₂ L W ε)
120+
121+
/-- The left unitor in the localized monoidal category `LocalizedMonoidal L W ε`. -/
122+
noncomputable def leftUnitor : (tensorBifunctor L W ε).obj unit ≅ 𝟭 _ :=
123+
(tensorBifunctor L W ε).mapIso ε.symm ≪≫
124+
Localization.liftNatIso L' W (tensorLeft (𝟙_ C) ⋙ L') L'
125+
((tensorBifunctor L W ε).obj ((L').obj (𝟙_ _))) _
126+
(isoWhiskerRight (leftUnitorNatIso C) _ ≪≫ L.leftUnitor)
127+
128+
/-- The right unitor in the localized monoidal category `LocalizedMonoidal L W ε`. -/
129+
noncomputable def rightUnitor : (tensorBifunctor L W ε).flip.obj unit ≅ 𝟭 _ :=
130+
(tensorBifunctor L W ε).flip.mapIso ε.symm ≪≫
131+
Localization.liftNatIso L' W (tensorRight (𝟙_ C) ⋙ L') L'
132+
((tensorBifunctor L W ε).flip.obj ((L').obj (𝟙_ _))) _
133+
(isoWhiskerRight (rightUnitorNatIso C) _ ≪≫ L.leftUnitor)
134+
135+
/-- The associator in the localized monoidal category `LocalizedMonoidal L W ε`. -/
136+
noncomputable def associator :
137+
bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε) ≅
138+
bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε) :=
139+
Localization.associator L' L' L' L' L' L' W W W W W
140+
(curriedAssociatorNatIso C) (tensorBifunctor L W ε) (tensorBifunctor L W ε)
141+
(tensorBifunctor L W ε) (tensorBifunctor L W ε)
142+
143+
noncomputable instance monoidalCategoryStruct :
144+
MonoidalCategoryStruct (LocalizedMonoidal L W ε) where
145+
tensorObj X Y := ((tensorBifunctor L W ε).obj X).obj Y
146+
whiskerLeft X _ _ g := ((tensorBifunctor L W ε).obj X).map g
147+
whiskerRight f Y := ((tensorBifunctor L W ε).map f).app Y
148+
tensorUnit := unit
149+
associator X Y Z := (((associator L W ε).app X).app Y).app Z
150+
leftUnitor Y := (leftUnitor L W ε).app Y
151+
rightUnitor X := (rightUnitor L W ε).app X
152+
153+
/-- The compatibility isomorphism of the monoidal functor `toMonoidalCategory L W ε`
154+
with respect to the tensor product. -/
155+
noncomputable def μ (X Y : C) : (L').obj X ⊗ (L').obj Y ≅ (L').obj (X ⊗ Y) :=
156+
((tensorBifunctorIso L W ε).app X).app Y
157+
158+
@[reassoc (attr := simp)]
159+
lemma μ_natural_left {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
160+
(L').map f ▷ (L').obj Y ≫ (μ L W ε X₂ Y).hom =
161+
(μ L W ε X₁ Y).hom ≫ (L').map (f ▷ Y) :=
162+
NatTrans.naturality_app (tensorBifunctorIso L W ε).hom Y f
163+
164+
@[reassoc (attr := simp)]
165+
lemma μ_inv_natural_left {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
166+
(μ L W ε X₁ Y).inv ≫ (L').map f ▷ (L').obj Y =
167+
(L').map (f ▷ Y) ≫ (μ L W ε X₂ Y).inv := by
168+
simp [Iso.eq_comp_inv]
169+
170+
@[reassoc (attr := simp)]
171+
lemma μ_natural_right (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
172+
(L').obj X ◁ (L').map g ≫ (μ L W ε X Y₂).hom =
173+
(μ L W ε X Y₁).hom ≫ (L').map (X ◁ g) :=
174+
((tensorBifunctorIso L W ε).hom.app X).naturality g
175+
176+
@[reassoc (attr := simp)]
177+
lemma μ_inv_natural_right (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
178+
(μ L W ε X Y₁).inv ≫ (L').obj X ◁ (L').map g =
179+
(L').map (X ◁ g) ≫ (μ L W ε X Y₂).inv := by
180+
simp [Iso.eq_comp_inv]
181+
182+
lemma leftUnitor_hom_app (Y : C) :
183+
(λ_ ((L').obj Y)).hom =
184+
(ε' L W ε).inv ▷ (L').obj Y ≫ (μ _ _ _ _ _).hom ≫ (L').map (λ_ Y).hom := by
185+
dsimp [monoidalCategoryStruct, leftUnitor]
186+
rw [liftNatTrans_app]
187+
dsimp
188+
rw [assoc]
189+
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
190+
simp only [comp_id]
191+
192+
lemma rightUnitor_hom_app (X : C) :
193+
(ρ_ ((L').obj X)).hom =
194+
(L').obj X ◁ (ε' L W ε).inv ≫ (μ _ _ _ _ _).hom ≫
195+
(L').map (ρ_ X).hom := by
196+
dsimp [monoidalCategoryStruct, rightUnitor]
197+
rw [liftNatTrans_app]
198+
dsimp
199+
rw [assoc]
200+
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
201+
simp only [comp_id]
202+
203+
lemma associator_hom_app (X₁ X₂ X₃ : C) :
204+
(α_ ((L').obj X₁) ((L').obj X₂) ((L').obj X₃)).hom =
205+
((μ L W ε _ _).hom ⊗ 𝟙 _) ≫ (μ L W ε _ _).hom ≫ (L').map (α_ X₁ X₂ X₃).hom ≫
206+
(μ L W ε _ _).inv ≫ (𝟙 _ ⊗ (μ L W ε _ _).inv) := by
207+
dsimp [monoidalCategoryStruct, associator]
208+
simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]
209+
rw [Localization.associator_hom_app_app_app]
210+
rfl
211+
212+
lemma id_tensorHom (X : LocalizedMonoidal L W ε) {Y₁ Y₂ : LocalizedMonoidal L W ε} (f : Y₁ ⟶ Y₂) :
213+
𝟙 X ⊗ f = X ◁ f := by
214+
simp [monoidalCategoryStruct]
215+
216+
lemma tensorHom_id {X₁ X₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ X₂) (Y : LocalizedMonoidal L W ε) :
217+
f ⊗ 𝟙 Y = f ▷ Y := by
218+
simp [monoidalCategoryStruct]
219+
220+
@[reassoc]
221+
lemma tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε}
222+
(f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
223+
(f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) := by
224+
simp [monoidalCategoryStruct]
225+
226+
lemma tensor_id (X₁ X₂ : LocalizedMonoidal L W ε) : 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂) := by
227+
simp [monoidalCategoryStruct]
228+
229+
@[reassoc]
230+
theorem whiskerLeft_comp (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε}
231+
(f : X ⟶ Y) (g : Y ⟶ Z) :
232+
Q ◁ (f ≫ g) = Q ◁ f ≫ Q ◁ g := by
233+
simp only [← id_tensorHom, ← tensor_comp, comp_id]
234+
235+
@[reassoc]
236+
theorem whiskerRight_comp (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε}
237+
(f : X ⟶ Y) (g : Y ⟶ Z) :
238+
(f ≫ g) ▷ Q = f ▷ Q ≫ g ▷ Q := by
239+
simp only [← tensorHom_id, ← tensor_comp, comp_id]
240+
241+
lemma whiskerLeft_id (X Y : LocalizedMonoidal L W ε) :
242+
X ◁ (𝟙 Y) = 𝟙 _ := by simp [monoidalCategoryStruct]
243+
244+
lemma whiskerRight_id (X Y : LocalizedMonoidal L W ε) :
245+
(𝟙 X) ▷ Y = 𝟙 _ := by simp [monoidalCategoryStruct]
246+
247+
@[reassoc]
248+
lemma whisker_exchange {Q X Y Z : LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z) :
249+
Q ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g := by
250+
simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]
251+
252+
@[reassoc]
253+
lemma associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε}
254+
(f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
255+
((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃) := by
256+
have h₁ := (((associator L W ε).hom.app Y₁).app Y₂).naturality f₃
257+
have h₂ := NatTrans.congr_app (((associator L W ε).hom.app Y₁).naturality f₂) X₃
258+
have h₃ := NatTrans.congr_app (NatTrans.congr_app ((associator L W ε).hom.naturality f₁) X₂) X₃
259+
simp only [monoidalCategoryStruct, Functor.map_comp, assoc]
260+
dsimp at h₁ h₂ h₃ ⊢
261+
rw [h₁, assoc, reassoc_of% h₂, reassoc_of% h₃]
262+
263+
@[reassoc]
264+
lemma associator_naturality₁ {X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) :
265+
((f₁ ▷ X₂) ▷ X₃) ≫ (α_ Y₁ X₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ▷ (X₂ ⊗ X₃)) := by
266+
simp only [← tensorHom_id, associator_naturality, Iso.cancel_iso_hom_left, tensor_id]
267+
268+
@[reassoc]
269+
lemma associator_naturality₂ {X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) :
270+
((X₁ ◁ f₂) ▷ X₃) ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (f₂ ▷ X₃)) := by
271+
simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]
272+
273+
@[reassoc]
274+
lemma associator_naturality₃ {X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) :
275+
((X₁ ⊗ X₂) ◁ f₃) ≫ (α_ X₁ X₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (X₂ ◁ f₃)) := by
276+
simp only [← id_tensorHom, ← tensor_id, associator_naturality]
277+
278+
end Monoidal
279+
280+
end Localization
281+
282+
end CategoryTheory

‎Mathlib/CategoryTheory/Whiskering.lean‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -370,7 +370,15 @@ def whiskeringLeft₃ :
370370
obj F₁ := whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁
371371
map τ₁ := whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁
372372

373-
variable {E} in
373+
variable {E}
374+
375+
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
376+
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'`. -/
377+
@[simps!]
378+
def Functor.postcompose₂ {E' : Type*} [Category E'] :
379+
(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E' :=
380+
whiskeringRight C₂ _ _ ⋙ whiskeringRight C₁ _ _
381+
374382
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
375383
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'`. -/
376384
@[simps!]
@@ -379,4 +387,3 @@ def Functor.postcompose₃ {E' : Type*} [Category E'] :
379387
whiskeringRight C₃ _ _ ⋙ whiskeringRight C₂ _ _ ⋙ whiskeringRight C₁ _ _
380388

381389
end CategoryTheory
382-

0 commit comments

Comments
 (0)