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.{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

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorFlipCurriedTensorObjWhiskeringRightTensorBifunctor {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).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.{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) [BraidedCategory C] : tensorBifunctor L W ε ≅ (tensorBifunctor L W ε).flip

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.

theorem CategoryTheory.Localization.Monoidal.braidingNatIso_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) [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.{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) [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.{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) [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.{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) [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.{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) [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.{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) [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.{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) [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.{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) [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.{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) [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))

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instBraidedCategoryLocalizedMonoidal {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) [BraidedCategory C] : BraidedCategory (LocalizedMonoidal L W ε)

Equations

• CategoryTheory.Localization.Monoidal.instBraidedCategoryLocalizedMonoidal L W ε = CategoryTheory.BraidedCategory.ofBifunctor (CategoryTheory.Localization.Monoidal.braidingNatIso L W ε) ⋯ ⋯

theorem CategoryTheory.Localization.Monoidal.β_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) [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))

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instBraidedLocalizedMonoidalToMonoidalCategory {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) [BraidedCategory C] : (toMonoidalCategory L W ε).Braided

Equations

• CategoryTheory.Localization.Monoidal.instBraidedLocalizedMonoidalToMonoidalCategory L W ε = { toMonoidal := CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory L W ε, braided := ⋯ }

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Monoidal.instSymmetricCategoryLocalizedMonoidal {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) [SymmetricCategory C] : SymmetricCategory (LocalizedMonoidal L W ε)

Equations

• CategoryTheory.Localization.Monoidal.instSymmetricCategoryLocalizedMonoidal L W ε = CategoryTheory.SymmetricCategory.ofCurried ⋯