Theorems · Definition · category theory

CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost

{C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (L : CategoryTheory.Functor C D) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [L.IsLocalization W] →
                        [L.Monoidal] →
                          (F : CategoryTheory.Functor D E) →
                            (G : CategoryTheory.Functor C E) →
                              [G.Monoidal] →
                                [W.ContainsIdentities] →
                                  [CategoryTheory.Localization.Lifting L W G F] →
                                    CategoryTheory.MonoidalCategory.curriedTensorPre F ≅
                                      CategoryTheory.MonoidalCategory.curriedTensorPost F

The natural isomorphism of bifunctors F - ⊗ F - ≅ F (- ⊗ -), given that F lifts along L to a monoidal functor G, where L is a monoidal localization functor.

Defined in

Mathlib.CategoryTheory.Localization.Monoidal.Functor

Cited by

6 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.MonoidalCategoryTheory.Functor.MonoidalCategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.Localization.Lifting