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.
instance
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
Equations
@[simp]
theorem
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
instance
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
Equations
@[simp]
theorem
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
noncomputable def
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
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
Instances For
theorem
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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₂))))
theorem
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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)))
theorem
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app'
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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)))))
noncomputable def
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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]
:
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
@[simp]
theorem
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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
@[simp]
theorem
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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
@[simp]
theorem
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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))
@[simp]
theorem
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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)))
noncomputable def
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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
theorem
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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)))
theorem
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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))
theorem
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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))))
theorem
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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)))
instance
CategoryTheory.Localization.Monoidal.lifting_isMonoidal
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, 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.