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.

The symmetric case is considered in the file Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean.

class CategoryTheory.MorphismProperty.IsMonoidal {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] extends W.IsMultiplicative : Prop

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.

• id_mem (X : C) : W (CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W g → W (CategoryStruct.comp f g)
• whiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (MonoidalCategoryStruct.whiskerLeft X g)
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : W f) (Y : C) : W (MonoidalCategoryStruct.whiskerRight f Y)

theorem CategoryTheory.MorphismProperty.IsMonoidal.mk' {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMultiplicative] (h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (MonoidalCategoryStruct.tensorHom f g)) : W.IsMonoidal

Alternative constructor for W.IsMonoidal given that W is multiplicative and stable under tensoring morphisms.

theorem CategoryTheory.MorphismProperty.whiskerLeft_mem {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (MonoidalCategoryStruct.whiskerLeft X g)

theorem CategoryTheory.MorphismProperty.whiskerRight_mem {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : W f) (Y : C) : W (MonoidalCategoryStruct.whiskerRight f Y)

theorem CategoryTheory.MorphismProperty.tensorHom_mem {C : Type u_1} [Category.{v_1, 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) : W (MonoidalCategoryStruct.tensorHom f g)

instance CategoryTheory.MorphismProperty.instIsMonoidalInverseImageOfMonoidalOfRespectsIso {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) [MonoidalCategory C] [W.IsMonoidal] {C' : Type u_3} [Category.{v_3, u_3} C'] [MonoidalCategory C'] (F : Functor C' C) [F.Monoidal] [W.RespectsIso] : (W.inverseImage F).IsMonoidal

The inverse image under a monoidal functor of a monoidal morphism property which respects isomorphisms is monoidal.

def CategoryTheory.LocalizedMonoidal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] (L : Functor C D) (W : MorphismProperty C) [W.IsMonoidal] [L.IsLocalization W] {unit : D} : (L.obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit) → Type u_2

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

• CategoryTheory.LocalizedMonoidal L W x✝ = D

@[instance_reducible]

instance CategoryTheory.Localization.instCategoryLocalizedMonoidal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : Category.{v_2, u_2} (LocalizedMonoidal L W ε)

Equations

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

def CategoryTheory.Localization.Monoidal.toMonoidalCategory {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : Functor C (LocalizedMonoidal L W ε)

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

Equations

• CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε = L

@[reducible, inline]

abbrev CategoryTheory.Localization.Monoidal.ε' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 ε).obj (MonoidalCategoryStruct.tensorUnit C) ≅ unit

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

Equations

• CategoryTheory.Localization.Monoidal.ε' L W ε = ε

instance CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

theorem CategoryTheory.Localization.Monoidal.isInvertedBy₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : W.IsInvertedBy₂ W ((MonoidalCategory.curriedTensor C).comp ((Functor.whiskeringRight C C D).obj (toMonoidalCategory L W ε)))

noncomputable def CategoryTheory.Localization.Monoidal.tensorBifunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : Functor (LocalizedMonoidal L W ε) (Functor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))

The localized tensor product, as a bifunctor.

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorCurriedTensorObjWhiskeringRightTensorBifunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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).comp ((Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj (toMonoidalCategory L W ε))) (tensorBifunctor L W ε)

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Localization.Monoidal.tensorBifunctorIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : (((Functor.whiskeringLeft₂ D).obj (toMonoidalCategory L W ε)).obj (toMonoidalCategory L W ε)).obj (tensorBifunctor L W ε) ≅ (Functor.postcompose₂.obj (toMonoidalCategory L W ε)).obj (MonoidalCategory.curriedTensor C)

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.

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorLeftObjFunctorTensorBifunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : Lifting (toMonoidalCategory L W ε) W ((MonoidalCategory.tensorLeft X).comp (toMonoidalCategory L W ε)) ((tensorBifunctor L W ε).obj ((toMonoidalCategory L W ε).obj X))

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorRightObjFunctorFlipTensorBifunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : Lifting (toMonoidalCategory L W ε) W ((MonoidalCategory.tensorRight Y).comp (toMonoidalCategory L W ε)) ((tensorBifunctor L W ε).flip.obj ((toMonoidalCategory L W ε).obj Y))

Equations

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

noncomputable def CategoryTheory.Localization.Monoidal.leftUnitor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : (tensorBifunctor L W ε).obj unit ≅ Functor.id (LocalizedMonoidal L W ε)

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

Equations

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

noncomputable def CategoryTheory.Localization.Monoidal.rightUnitor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : (tensorBifunctor L W ε).flip.obj unit ≅ Functor.id (LocalizedMonoidal L W ε)

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

Equations

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

noncomputable def CategoryTheory.Localization.Monoidal.associator {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε) ≅ bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)

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

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.monoidalCategoryStruct {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : MonoidalCategoryStruct (LocalizedMonoidal L W ε)

Equations

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

noncomputable def CategoryTheory.Localization.Monoidal.μ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y) ≅ (toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X Y)

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

Equations

• CategoryTheory.Localization.Monoidal.μ L W ε X Y = ((CategoryTheory.Localization.Monoidal.tensorBifunctorIso L W ε).app X).app Y

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_natural_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((toMonoidalCategory L W ε).map f) ((toMonoidalCategory L W ε).obj Y)) (μ L W ε X₂ Y).hom = CategoryStruct.comp (μ L W ε X₁ Y).hom ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerRight f Y))

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_natural_left_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : LocalizedMonoidal L W ε} (h : (toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X₂ Y) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((toMonoidalCategory L W ε).map f) ((toMonoidalCategory L W ε).obj Y)) (CategoryStruct.comp (μ L W ε X₂ Y).hom h) = CategoryStruct.comp (μ L W ε X₁ Y).hom (CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerRight f Y)) h)

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_inv_natural_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : CategoryStruct.comp (μ L W ε X₁ Y).inv (MonoidalCategoryStruct.whiskerRight ((toMonoidalCategory L W ε).map f) ((toMonoidalCategory L W ε).obj Y)) = CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerRight f Y)) (μ L W ε X₂ Y).inv

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_inv_natural_left_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X₂) ((toMonoidalCategory L W ε).obj Y) ⟶ Z) : CategoryStruct.comp (μ L W ε X₁ Y).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((toMonoidalCategory L W ε).map f) ((toMonoidalCategory L W ε).obj Y)) h) = CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerRight f Y)) (CategoryStruct.comp (μ L W ε X₂ Y).inv h)

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_natural_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).map g)) (μ L W ε X Y₂).hom = CategoryStruct.comp (μ L W ε X Y₁).hom ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerLeft X g))

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_natural_right_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : LocalizedMonoidal L W ε} (h : (toMonoidalCategory L W ε).obj (MonoidalCategoryStruct.tensorObj X Y₂) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).map g)) (CategoryStruct.comp (μ L W ε X Y₂).hom h) = CategoryStruct.comp (μ L W ε X Y₁).hom (CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerLeft X g)) h)

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_inv_natural_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (μ L W ε X Y₁).inv (MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).map g)) = CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerLeft X g)) (μ L W ε X Y₂).inv

@[simp]

theorem CategoryTheory.Localization.Monoidal.μ_inv_natural_right_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y₂) ⟶ Z) : CategoryStruct.comp (μ L W ε X Y₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).map g)) h) = CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.whiskerLeft X g)) (CategoryStruct.comp (μ L W ε X Y₂).inv h)

theorem CategoryTheory.Localization.Monoidal.leftUnitor_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : (MonoidalCategoryStruct.leftUnitor ((toMonoidalCategory L W ε).obj Y)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε' L W ε).inv ((toMonoidalCategory L W ε).obj Y)) (CategoryStruct.comp (μ L W ε (MonoidalCategoryStruct.tensorUnit C) Y).hom ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.leftUnitor Y).hom))

theorem CategoryTheory.Localization.Monoidal.rightUnitor_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : (MonoidalCategoryStruct.rightUnitor ((toMonoidalCategory L W ε).obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X) (ε' L W ε).inv) (CategoryStruct.comp (μ L W ε X (MonoidalCategoryStruct.tensorUnit C)).hom ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.rightUnitor X).hom))

theorem CategoryTheory.Localization.Monoidal.associator_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ : C) : (MonoidalCategoryStruct.associator ((toMonoidalCategory L W ε).obj X₁) ((toMonoidalCategory L W ε).obj X₂) ((toMonoidalCategory L W ε).obj X₃)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ L W ε X₁ X₂).hom (CategoryStruct.id ((toMonoidalCategory L W ε).obj X₃))) (CategoryStruct.comp (μ L W ε (MonoidalCategoryStruct.tensorObj X₁ X₂) X₃).hom (CategoryStruct.comp ((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom) (CategoryStruct.comp (μ L W ε X₁ (MonoidalCategoryStruct.tensorObj X₂ X₃)).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.id ((toMonoidalCategory L W ε).obj X₁)) (μ L W ε X₂ X₃).inv))))

theorem CategoryTheory.Localization.Monoidal.id_tensorHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε) {Y₁ Y₂ : LocalizedMonoidal L W ε} (f : Y₁ ⟶ Y₂) : MonoidalCategoryStruct.tensorHom (CategoryStruct.id X) f = MonoidalCategoryStruct.whiskerLeft X f

theorem CategoryTheory.Localization.Monoidal.tensorHom_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ X₂) (Y : LocalizedMonoidal L W ε) : MonoidalCategoryStruct.tensorHom f (CategoryStruct.id Y) = MonoidalCategoryStruct.whiskerRight f Y

theorem CategoryTheory.Localization.Monoidal.tensor_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₂) : MonoidalCategoryStruct.tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f₁ f₂) (MonoidalCategoryStruct.tensorHom g₁ g₂)

theorem CategoryTheory.Localization.Monoidal.tensor_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)) h = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f₁ f₂) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g₁ g₂) h)

theorem CategoryTheory.Localization.Monoidal.id_tensorHom_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ : LocalizedMonoidal L W ε) : MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X₁ X₂)

theorem CategoryTheory.Localization.Monoidal.whiskerLeft_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z) : MonoidalCategoryStruct.whiskerLeft Q (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q f) (MonoidalCategoryStruct.whiskerLeft Q g)

theorem CategoryTheory.Localization.Monoidal.whiskerLeft_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj Q Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q f) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q g) h)

theorem CategoryTheory.Localization.Monoidal.whiskerRight_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z) : MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp f g) Q = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Q) (MonoidalCategoryStruct.whiskerRight g Q)

theorem CategoryTheory.Localization.Monoidal.whiskerRight_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj Z Q ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp f g) Q) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Q) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight g Q) h)

theorem CategoryTheory.Localization.Monoidal.whiskerLeft_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε) : MonoidalCategoryStruct.whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)

theorem CategoryTheory.Localization.Monoidal.whiskerRight_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε) : MonoidalCategoryStruct.whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)

theorem CategoryTheory.Localization.Monoidal.whisker_exchange {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) {Q X Y Z : LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q g) (MonoidalCategoryStruct.whiskerRight f Z) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (MonoidalCategoryStruct.whiskerLeft X g)

theorem CategoryTheory.Localization.Monoidal.whisker_exchange_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) {Q X Y Z : LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z) {Z✝ : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Q g) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) h)

theorem CategoryTheory.Localization.Monoidal.associator_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f₁ f₂) f₃) (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (MonoidalCategoryStruct.tensorHom f₁ (MonoidalCategoryStruct.tensorHom f₂ f₃))

theorem CategoryTheory.Localization.Monoidal.associator_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj Y₁ (MonoidalCategoryStruct.tensorObj Y₂ Y₃) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f₁ f₂) f₃) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f₁ (MonoidalCategoryStruct.tensorHom f₂ f₃)) h)

theorem CategoryTheory.Localization.Monoidal.associator_naturality₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f₁ X₂) X₃) (MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (MonoidalCategoryStruct.whiskerRight f₁ (MonoidalCategoryStruct.tensorObj X₂ X₃))

theorem CategoryTheory.Localization.Monoidal.associator_naturality₁_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj Y₁ (MonoidalCategoryStruct.tensorObj X₂ X₃) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f₁ X₂) X₃) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f₁ (MonoidalCategoryStruct.tensorObj X₂ X₃)) h)

theorem CategoryTheory.Localization.Monoidal.associator_naturality₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerLeft X₁ f₂) X₃) (MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight f₂ X₃))

theorem CategoryTheory.Localization.Monoidal.associator_naturality₂_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj X₁ (MonoidalCategoryStruct.tensorObj Y₂ X₃) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerLeft X₁ f₂) X₃) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight f₂ X₃)) h)

theorem CategoryTheory.Localization.Monoidal.associator_naturality₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj X₁ X₂) f₃) (MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₂ f₃))

theorem CategoryTheory.Localization.Monoidal.associator_naturality₃_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) {Z : LocalizedMonoidal L W ε} (h : MonoidalCategoryStruct.tensorObj X₁ (MonoidalCategoryStruct.tensorObj X₂ Y₃) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj X₁ X₂) f₃) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₂ f₃)) h)

instance CategoryTheory.Localization.Monoidal.instEssSurjLocalizedMonoidalToMonoidalCategory {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 ε).EssSurj

theorem CategoryTheory.Localization.Monoidal.pentagon_natTrans {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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} : MonoidalCategory.ofBifunctor.Pentagon.firstMap (tensorBifunctor L W ε) (associator L W ε) = MonoidalCategory.ofBifunctor.Pentagon.secondMap (tensorBifunctor L W ε) (associator L W ε)

The two paths around the localized monoidal pentagon agree as natural transformations of quadrifunctors.

theorem CategoryTheory.Localization.Monoidal.pentagon {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₄

The pointwise pentagon identity in the localized monoidal category.

theorem CategoryTheory.Localization.Monoidal.leftUnitor_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε} (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit (LocalizedMonoidal L W ε)) f) (MonoidalCategoryStruct.leftUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom f

theorem CategoryTheory.Localization.Monoidal.rightUnitor_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε} (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit (LocalizedMonoidal L W ε))) (MonoidalCategoryStruct.rightUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom f

theorem CategoryTheory.Localization.Monoidal.triangle_natTrans {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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} : MonoidalCategory.ofBifunctor.Triangle.firstMap (tensorBifunctor L W ε) unit (associator L W ε) (leftUnitor L W ε) = MonoidalCategory.ofBifunctor.Triangle.secondMap (tensorBifunctor L W ε) unit (rightUnitor L W ε)

The two paths around the localized monoidal triangle agree as natural transformations of bifunctors.

theorem CategoryTheory.Localization.Monoidal.triangle {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : LocalizedMonoidal L W ε) : CategoryStruct.comp (MonoidalCategoryStruct.associator X (MonoidalCategoryStruct.tensorUnit (LocalizedMonoidal L W ε)) Y).hom (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.leftUnitor Y).hom) = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.rightUnitor X).hom Y

The pointwise triangle identity in the localized monoidal category.

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instMonoidalCategoryLocalizedMonoidal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : MonoidalCategory (LocalizedMonoidal L W ε)

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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) : (Localization.Monoidal.toMonoidalCategory L W ε).Monoidal

Equations

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

theorem CategoryTheory.associator_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : (MonoidalCategoryStruct.associator ((Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ (Localization.Monoidal.toMonoidalCategory L W ε) X Y) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Z)) (CategoryStruct.comp (Functor.LaxMonoidal.μ (Localization.Monoidal.toMonoidalCategory L W ε) (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp ((Localization.Monoidal.toMonoidalCategory L W ε).map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (Functor.OplaxMonoidal.δ (Localization.Monoidal.toMonoidalCategory L W ε) X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft ((Localization.Monoidal.toMonoidalCategory L W ε).obj X) (Functor.OplaxMonoidal.δ (Localization.Monoidal.toMonoidalCategory L W ε) Y Z)))))

theorem CategoryTheory.associator_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 : C) : (MonoidalCategoryStruct.associator ((Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).inv = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((Localization.Monoidal.toMonoidalCategory L W ε).obj X) (Functor.LaxMonoidal.μ (Localization.Monoidal.toMonoidalCategory L W ε) Y Z)) (CategoryStruct.comp (Functor.LaxMonoidal.μ (Localization.Monoidal.toMonoidalCategory L W ε) X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp ((Localization.Monoidal.toMonoidalCategory L W ε).map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (Functor.OplaxMonoidal.δ (Localization.Monoidal.toMonoidalCategory L W ε) (MonoidalCategoryStruct.tensorObj X Y) Z) (MonoidalCategoryStruct.whiskerRight (Functor.OplaxMonoidal.δ (Localization.Monoidal.toMonoidalCategory L W ε) X Y) ((Localization.Monoidal.toMonoidalCategory L W ε).obj Z)))))