Documentation

Mathlib.CategoryTheory.Localization.Monoidal

Localization of monoidal categories #

Let C be a monoidal category equipped with a class of morphisms W which is compatible with the monoidal category structure: this means W is multiplicative and stable by left and right whiskerings (this is the type class W.IsMonoidal). Let L : C ⥤ D be a localization functor for W. In the file, we construct a monoidal category structure on D such that the localization functor is monoidal. The structure is actually defined on a type synonym LocalizedMonoidal L W ε. Here, the data ε : L.obj (𝟙_ C) ≅ unit is an isomorphism to some object unit : D which allows the user to provide a preferred choice of a unit object.

A class of morphisms W in a monoidal category is monoidal if it is multiplicative and stable under left and right whiskering. Under this condition, the localized category can be equipped with a monoidal category structure, see LocalizedMonoidal.

Instances
    theorem CategoryTheory.MorphismProperty.whiskerLeft_mem {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] (X : C) {Y₁ Y₂ : C} (g : Y₁ Y₂) (hg : W g) :
    theorem CategoryTheory.MorphismProperty.whiskerRight_mem {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] {X₁ X₂ : C} (f : X₁ X₂) (hf : W f) (Y : C) :
    theorem CategoryTheory.MorphismProperty.tensorHom_mem {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] {X₁ X₂ : C} (f : X₁ X₂) {Y₁ Y₂ : C} (g : Y₁ Y₂) (hf : W f) (hg : W g) :

    Given a monoidal category C, a localization functor L : C ⥤ D with respect to W : MorphismProperty C which satisfies W.IsMonoidal, and a choice of object unit : D with an isomorphism L.obj (𝟙_ C) ≅ unit, this is a type synonym for D on which we define the localized monoidal category structure.

    Equations

    The monoidal functor from a monoidal category C to its localization LocalizedMonoidal L W ε.

    Equations
    @[reducible, inline]

    The isomorphism ε : L.obj (𝟙_ C) ≅ unit, as (toMonoidalCategory L W ε).obj (𝟙_ C) ≅ unit.

    Equations

    The localized tensor product, as a bifunctor.

    Equations
    • One or more equations did not get rendered due to their size.
    @[reducible, inline]

    The bifunctor tensorBifunctor on LocalizedMonoidal L W ε is induced by curriedTensor C.

    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.

    The left unitor in the localized monoidal category LocalizedMonoidal L W ε.

    Equations
    • One or more equations did not get rendered due to their size.

    The right unitor in the localized monoidal category LocalizedMonoidal L W ε.

    Equations
    • One or more equations did not get rendered due to their size.

    The associator in the localized monoidal category LocalizedMonoidal L W ε.

    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.

    The compatibility isomorphism of the monoidal functor toMonoidalCategory L W ε with respect to the tensor product.

    Equations
    theorem CategoryTheory.Localization.Monoidal.tensor_comp {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) {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
    theorem CategoryTheory.Localization.Monoidal.tensor_comp_assoc {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) {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj Z₁ Z₂ Z) :
    theorem CategoryTheory.Localization.Monoidal.pentagon {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} (Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε) :
    MonoidalCategory.Pentagon Y₁ Y₂ Y₃ Y₄
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.