Localization of symmetric monoidal categories #
Let C be a monoidal category equipped with a class of morphisms W which
is compatible with the monoidal category structure. The file
Mathlib.CategoryTheory.Localization.Monoidal.Basic constructs a monoidal structure on
the localized on D such that the localization functor is monoidal.
In this file we promote this monoidal structure to a braided structure in the case where C is
braided, in such a way that the localization functor is braided. If C is symmetric monoidal, then
the monoidal structure on D is also symmetric.
instance
CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
:
(toMonoidalCategory L W ε).IsLocalization W
noncomputable instance
CategoryTheory.Localization.Monoidal.instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorFlipCurriedTensorObjWhiskeringRightTensorBifunctor
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
:
Lifting₂ (toMonoidalCategory L W ε) (toMonoidalCategory L W ε) W W
((MonoidalCategory.curriedTensor C).flip.comp
((Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj (toMonoidalCategory L W ε)))
(tensorBifunctor L W ε).flip
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Localization.Monoidal.braidingNatIso
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
:
The braiding on the localized category as a natural isomorphism of bifunctors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y : C)
:
((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Y) = CategoryStruct.comp (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y)
(CategoryStruct.comp ((toMonoidalCategory L W ε).map (β_ X Y).hom)
(Functor.OplaxMonoidal.δ (toMonoidalCategory L W ε) Y X))
theorem
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
:
CategoryStruct.comp
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj X)).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)))
(MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) Y Z)
((toMonoidalCategory L W ε).obj X)) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X)
(Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) Y Z))
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj X)).app
((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj Y Z)))
theorem
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
{Z✝ : LocalizedMonoidal L W ε}
(h :
MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj Y Z))
((toMonoidalCategory L W ε).obj X) ⟶ Z✝)
:
CategoryStruct.comp
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj X)).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)))
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) Y Z)
((toMonoidalCategory L W ε).obj X))
h) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X)
(Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) Y Z))
(CategoryStruct.comp
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj X)).app
((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj Y Z)))
h)
theorem
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
:
CategoryStruct.comp
(((braidingNatIso L W ε).hom.app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y))).app
((toMonoidalCategory L W ε).obj Z))
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj Z)
(Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y)) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y)
((toMonoidalCategory L W ε).obj Z))
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X Y))).app
((toMonoidalCategory L W ε).obj Z))
theorem
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
{Z✝ : LocalizedMonoidal L W ε}
(h :
MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Z)
((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z✝)
:
CategoryStruct.comp
(((braidingNatIso L W ε).hom.app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y))).app
((toMonoidalCategory L W ε).obj Z))
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj Z)
(Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y))
h) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y)
((toMonoidalCategory L W ε).obj Z))
(CategoryStruct.comp
(((braidingNatIso L W ε).hom.app ((toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X Y))).app
((toMonoidalCategory L W ε).obj Z))
h)
theorem
CategoryTheory.Localization.Monoidal.map_hexagon_forward
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
:
CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y)
((toMonoidalCategory L W ε).obj Z)).hom
(CategoryStruct.comp
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z))).hom
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)
((toMonoidalCategory L W ε).obj X)).hom) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Y)).hom
((toMonoidalCategory L W ε).obj Z))
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Z)).hom
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj Y)
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Z)).hom))
theorem
CategoryTheory.Localization.Monoidal.map_hexagon_forward_assoc
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
{Z✝ : LocalizedMonoidal L W ε}
(h :
MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Y)
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Z) ((toMonoidalCategory L W ε).obj X)) ⟶ Z✝)
:
CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y)
((toMonoidalCategory L W ε).obj Z)).hom
(CategoryStruct.comp
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z))).hom
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)
((toMonoidalCategory L W ε).obj X)).hom
h)) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Y)).hom
((toMonoidalCategory L W ε).obj Z))
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Z)).hom
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj Y)
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Z)).hom)
h))
theorem
CategoryTheory.Localization.Monoidal.map_hexagon_reverse
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
:
CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y)
((toMonoidalCategory L W ε).obj Z)).inv
(CategoryStruct.comp
(((braidingNatIso L W ε).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Y))).app
((toMonoidalCategory L W ε).obj Z)).hom
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Z) ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Y)).inv) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X)
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj Y)).app ((toMonoidalCategory L W ε).obj Z)).hom)
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Z)
((toMonoidalCategory L W ε).obj Y)).inv
(MonoidalCategoryStruct.whiskerRight
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Z)).hom
((toMonoidalCategory L W ε).obj Y)))
theorem
CategoryTheory.Localization.Monoidal.map_hexagon_reverse_assoc
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y Z : C)
{Z✝ : LocalizedMonoidal L W ε}
(h :
MonoidalCategoryStruct.tensorObj
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj Z) ((toMonoidalCategory L W ε).obj X))
((toMonoidalCategory L W ε).obj Y) ⟶ Z✝)
:
CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y)
((toMonoidalCategory L W ε).obj Z)).inv
(CategoryStruct.comp
(((braidingNatIso L W ε).app
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Y))).app
((toMonoidalCategory L W ε).obj Z)).hom
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj Z) ((toMonoidalCategory L W ε).obj X)
((toMonoidalCategory L W ε).obj Y)).inv
h)) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X)
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj Y)).app ((toMonoidalCategory L W ε).obj Z)).hom)
(CategoryStruct.comp
(MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Z)
((toMonoidalCategory L W ε).obj Y)).inv
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight
(((braidingNatIso L W ε).app ((toMonoidalCategory L W ε).obj X)).app ((toMonoidalCategory L W ε).obj Z)).hom
((toMonoidalCategory L W ε).obj Y))
h))
noncomputable instance
CategoryTheory.Localization.Monoidal.instBraidedCategoryLocalizedMonoidal
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
:
BraidedCategory (LocalizedMonoidal L W ε)
theorem
CategoryTheory.Localization.Monoidal.β_hom_app
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
(X Y : C)
:
(β_ ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y)).hom = CategoryStruct.comp (Functor.LaxMonoidal.μ (toMonoidalCategory L W ε) X Y)
(CategoryStruct.comp ((toMonoidalCategory L W ε).map (β_ X Y).hom)
(Functor.OplaxMonoidal.δ (toMonoidalCategory L W ε) Y X))
noncomputable instance
CategoryTheory.Localization.Monoidal.instBraidedLocalizedMonoidalToMonoidalCategory
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[BraidedCategory C]
:
(toMonoidalCategory L W ε).Braided
Equations
- CategoryTheory.Localization.Monoidal.instBraidedLocalizedMonoidalToMonoidalCategory L W ε = { toMonoidal := CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory L W ε, braided := ⋯ }
noncomputable instance
CategoryTheory.Localization.Monoidal.instSymmetricCategoryLocalizedMonoidal
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(L : Functor C D)
(W : MorphismProperty C)
[MonoidalCategory C]
[W.IsMonoidal]
[L.IsLocalization W]
{unit : D}
(ε : L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit)
[SymmetricCategory C]
:
SymmetricCategory (LocalizedMonoidal L W ε)