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 :
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.
- 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)
Instances
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))
:
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)
:
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)
:
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.
Instances For
@[implicit_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 ε)
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 ε.
Instances For
@[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)
:
The isomorphism ε : L.obj (𝟙_ C) ≅ unit,
as (toMonoidalCategory L W ε).obj (𝟙_ C) ≅ unit.
Instances For
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.
Instances For
@[implicit_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 ε)
@[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.
Instances For
@[implicit_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))
@[implicit_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))
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)
:
The left unitor in the localized monoidal category LocalizedMonoidal L W ε.
Instances For
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)
:
The right unitor in the localized monoidal category LocalizedMonoidal L W ε.
Instances For
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 ε.
Instances For
@[implicit_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)
:
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.
Instances For
@[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₂)
:
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 ε)
:
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 ε)
:
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)
:
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✝)
:
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)
:
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✝)
:
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 ε)
:
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 ε)
:
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)
:
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✝)
:
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₃)
:
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)
theorem
CategoryTheory.Localization.Monoidal.pentagon_aux₁
{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 ε}
(i : X₁ ≅ Y₁)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight i.hom X₂) X₃)
(CategoryStruct.comp (MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom
(MonoidalCategoryStruct.whiskerRight i.inv (MonoidalCategoryStruct.tensorObj X₂ X₃))) = (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
theorem
CategoryTheory.Localization.Monoidal.pentagon_aux₂
{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 ε}
(i : X₂ ≅ Y₂)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerLeft X₁ i.hom) X₃)
(CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom
(MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight i.inv X₃))) = (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
theorem
CategoryTheory.Localization.Monoidal.pentagon_aux₃
{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 ε}
(i : X₃ ≅ Y₃)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj X₁ X₂) i.hom)
(CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom
(MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₂ i.inv))) = (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
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
{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₄
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)
:
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)
:
theorem
CategoryTheory.Localization.Monoidal.triangle_aux₁
{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 ε}
(i₁ : X₁ ≅ Y₁)
(i₂ : X₂ ≅ Y₂)
(i₃ : X₃ ≅ Y₃)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom i₁.hom i₂.hom) i₃.hom)
(CategoryStruct.comp (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom
(MonoidalCategoryStruct.tensorHom i₁.inv (MonoidalCategoryStruct.tensorHom i₂.inv i₃.inv))) = (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
theorem
CategoryTheory.Localization.Monoidal.triangle_aux₁_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 ε}
(i₁ : X₁ ≅ Y₁)
(i₂ : X₂ ≅ Y₂)
(i₃ : X₃ ≅ Y₃)
{Z : LocalizedMonoidal L W ε}
(h : MonoidalCategoryStruct.tensorObj X₁ (MonoidalCategoryStruct.tensorObj X₂ X₃) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom i₁.hom i₂.hom) i₃.hom)
(CategoryStruct.comp (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom i₁.inv (MonoidalCategoryStruct.tensorHom i₂.inv i₃.inv))
h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom h
theorem
CategoryTheory.Localization.Monoidal.triangle_aux₂
{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 ε}
{X' Y' : C}
(e₁ : (toMonoidalCategory L W ε).obj X' ≅ X)
(e₂ : (toMonoidalCategory L W ε).obj Y' ≅ Y)
:
MonoidalCategoryStruct.tensorHom e₁.hom
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε.hom e₂.hom) (MonoidalCategoryStruct.leftUnitor Y).hom) = CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft ((toMonoidalCategory L W ε).obj X')
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε' L W ε).hom ((toMonoidalCategory L W ε).obj Y'))
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit (LocalizedMonoidal L W ε)) e₂.hom)
(MonoidalCategoryStruct.leftUnitor Y).hom)))
(MonoidalCategoryStruct.whiskerRight e₁.hom Y)
theorem
CategoryTheory.Localization.Monoidal.triangle_aux₃
{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 ε}
{X' Y' : C}
(e₁ : (toMonoidalCategory L W ε).obj X' ≅ X)
(e₂ : (toMonoidalCategory L W ε).obj Y' ≅ Y)
:
MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.rightUnitor X).hom Y = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom e₁.inv ε.inv) e₂.inv)
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerLeft
(MonoidalCategoryStruct.tensorObj ((toMonoidalCategory L W ε).obj X')
(L.obj (MonoidalCategoryStruct.tensorUnit C)))
e₂.hom)
(CategoryStruct.comp
(MonoidalCategoryStruct.whiskerRight
(CategoryStruct.comp (μ L W ε X' (MonoidalCategoryStruct.tensorUnit C)).hom
((toMonoidalCategory L W ε).map (MonoidalCategoryStruct.rightUnitor X').hom))
Y)
(MonoidalCategoryStruct.whiskerRight e₁.hom Y)))
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 ε)
:
@[implicit_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 ε)
@[implicit_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)
:
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)))))