Documentation

Mathlib.CategoryTheory.Localization.Monoidal.Functor

Universal property of localized monoidal categories #

This file proves that, given a monoidal localization functor L : C ⥤ D, and a functor F : D ⥤ E to a monoidal category, such that F lifts along L to a monoidal functor G, then F is monoidal. See CategoryTheory.Localization.Monoidal.functorMonoidalOfComp.

source
instance CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) (F : Functor D E) (G : Functor C E) [Lifting L W G F] :
Lifting₂ L L W W (MonoidalCategory.curriedTensorPre G) (MonoidalCategory.curriedTensorPre F)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) (F : Functor D E) (G : Functor C E) [Lifting L W G F] :
Lifting₂.iso L L W W (MonoidalCategory.curriedTensorPre G) (MonoidalCategory.curriedTensorPre F) = MonoidalCategory.curriedTensorPreFunctor.mapIso (Lifting.iso L W G F)
source
instance CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] (L : Functor C D) (W : MorphismProperty C) [L.Monoidal] (F : Functor D E) (G : Functor C E) [Lifting L W G F] :
Lifting₂ L L W W (MonoidalCategory.curriedTensorPost G) (MonoidalCategory.curriedTensorPost F)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] (L : Functor C D) (W : MorphismProperty C) [L.Monoidal] (F : Functor D E) (G : Functor C E) [Lifting L W G F] :
Lifting₂.iso L L W W (MonoidalCategory.curriedTensorPost G) (MonoidalCategory.curriedTensorPost F) = (Functor.postcompose₂.obj F).mapIso (MonoidalCategory.Functor.curriedTensorPreIsoPost L) ≪≫ MonoidalCategory.curriedTensorPostFunctor.mapIso (Lifting.iso L W G F)
source
noncomputable def CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
MonoidalCategory.curriedTensorPre F ≅ 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X₁ X₂ : C) :
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((Lifting.iso L W G F).hom.app X₁) ((Lifting.iso L W G F).hom.app X₂)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G X₁ X₂) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorObj X₁ X₂)) (F.map (Functor.OplaxMonoidal.δ L X₁ X₂))))
    source
    theorem CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X₁ X₂ : C) {Z : E} (h : ((MonoidalCategory.curriedTensorPost F).obj (L.obj X₁)).obj (L.obj X₂) ⟶ Z) :
    CategoryStruct.comp (((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂)) h = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((Lifting.iso L W G F).hom.app X₁) ((Lifting.iso L W G F).hom.app X₂)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G X₁ X₂) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorObj X₁ X₂)) (CategoryStruct.comp (F.map (Functor.OplaxMonoidal.δ L X₁ X₂)) h)))
    source
    theorem CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app' {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] {X₁ X₂ : C} {Y₁ Y₂ : D} (e₁ : Y₁ ≅ L.obj X₁) (e₂ : Y₂ ≅ L.obj X₂) :
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (F.map e₁.hom) ((Lifting.iso L W G F).hom.app X₁)) (CategoryStruct.comp (F.map e₂.hom) ((Lifting.iso L W G F).hom.app X₂))) (CategoryStruct.comp (Functor.LaxMonoidal.μ G X₁ X₂) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorObj X₁ X₂)) (F.map (CategoryStruct.comp (Functor.OplaxMonoidal.δ L X₁ X₂) (MonoidalCategoryStruct.tensorHom e₁.inv e₂.inv)))))
    source
    noncomputable def CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
    F.CoreMonoidal

    Monoidal structure on F, given that F lifts along L to a monoidal functor G, where L is a monoidal localization functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
      (functorCoreMonoidalOfComp L W F G).εIso.inv = CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε L)) (CategoryStruct.comp ((Lifting.iso L W G F).hom.app (MonoidalCategoryStruct.tensorUnit C)) (Functor.OplaxMonoidal.η G))
      source
      @[simp]
      theorem CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
      (functorCoreMonoidalOfComp L W F G).εIso.hom = CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorUnit C)) (F.map (Functor.OplaxMonoidal.η L)))
      source
      @[simp]
      theorem CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X Y : D) :
      ((functorCoreMonoidalOfComp L W F G).μIso X Y).hom = ((curriedTensorPreIsoPost L W F G).hom.app X).app Y
      source
      @[simp]
      theorem CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X Y : D) :
      ((functorCoreMonoidalOfComp L W F G).μIso X Y).inv = ((curriedTensorPreIsoPost L W F G).inv.app X).app Y
      source
      noncomputable def CategoryTheory.Localization.Monoidal.functorMonoidalOfComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
      F.Monoidal

      Monoidal structure on F, given that F lifts along L to a monoidal functor G, where L is a monoidal localization functor.

      Equations
      Instances For
        source
        theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
        Functor.LaxMonoidal.ε F = CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorUnit C)) (F.map (Functor.OplaxMonoidal.η L)))
        source
        theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] {Z : E} (h : F.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) :
        CategoryStruct.comp (Functor.LaxMonoidal.ε F) h = CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (F.map (Functor.OplaxMonoidal.η L)) h))
        source
        theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X Y : C) :
        Functor.LaxMonoidal.μ F (L.obj X) (L.obj Y) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((Lifting.iso L W G F).hom.app X) ((Lifting.iso L W G F).hom.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G X Y) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorObj X Y)) (F.map (Functor.OplaxMonoidal.δ L X Y))))
        source
        theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Category.{u_4, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] (X Y : C) {Z : E} (h : F.obj (MonoidalCategoryStruct.tensorObj (L.obj X) (L.obj Y)) ⟶ Z) :
        CategoryStruct.comp (Functor.LaxMonoidal.μ F (L.obj X) (L.obj Y)) h = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((Lifting.iso L W G F).hom.app X) ((Lifting.iso L W G F).hom.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G X Y) (CategoryStruct.comp ((Lifting.iso L W G F).inv.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (F.map (Functor.OplaxMonoidal.δ L X Y)) h)))
        source
        instance CategoryTheory.Localization.Monoidal.lifting_isMonoidal {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} E] [MonoidalCategory C] [MonoidalCategory D] [MonoidalCategory E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Monoidal] (F : Functor D E) (G : Functor C E) [G.Monoidal] [W.ContainsIdentities] [Lifting L W G F] :
        NatTrans.IsMonoidal (Lifting.iso L W G F).hom

        When F is given the monoidal structure functorMonoidalOfComp that is obtained by lifting along a monoidal localization functor L, then the lifting isomorphism is a monoidal natural transformation.