Compatibility lemmas for limits and colimits in a monoidal category #
For numerous simp lemmas of the form f ≫ g = h, we add accompanying simp lemmas of the form
Q ◁ f ≫ Q ◁ g = Q ◁ h and f ▷ Q ≫ g ▷ Q = h ▷ Q. This file and
Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback are needed to define a monoidal category
structure in Mathlib.CategoryTheory.Monoidal.Arrow.
TODO #
An attribute should be developed to automatically generate lemmas of this form.
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.HasColimit.whiskerLeft_isoOfNatIso_ι_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F G : Functor J C}
[Limits.HasColimit F]
[Limits.HasColimit G]
(w : F ≅ G)
(j : J)
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q (Limits.colimit.ι F j)) (whiskerLeft Q (Limits.HasColimit.isoOfNatIso w).hom) = CategoryStruct.comp (whiskerLeft Q (w.hom.app j)) (whiskerLeft Q (Limits.colimit.ι G j))
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.HasColimit.whiskerLeft_isoOfNatIso_ι_hom_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F G : Functor J C}
[Limits.HasColimit F]
[Limits.HasColimit G]
(w : F ≅ G)
(j : J)
{Q Z : C}
(h : tensorObj Q (Limits.colimit G) ⟶ Z)
:
CategoryStruct.comp (whiskerLeft Q (Limits.colimit.ι F j))
(CategoryStruct.comp (whiskerLeft Q (Limits.HasColimit.isoOfNatIso w).hom) h) = CategoryStruct.comp (whiskerLeft Q (w.hom.app j)) (CategoryStruct.comp (whiskerLeft Q (Limits.colimit.ι G j)) h)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.HasColimit.isoOfNatIso_ι_hom_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F G : Functor J C}
[Limits.HasColimit F]
[Limits.HasColimit G]
(w : F ≅ G)
(j : J)
{Q : C}
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι F j) Q) (whiskerRight (Limits.HasColimit.isoOfNatIso w).hom Q) = CategoryStruct.comp (whiskerRight (w.hom.app j) Q) (whiskerRight (Limits.colimit.ι G j) Q)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.HasColimit.isoOfNatIso_ι_hom_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F G : Functor J C}
[Limits.HasColimit F]
[Limits.HasColimit G]
(w : F ≅ G)
(j : J)
{Q Z : C}
(h : tensorObj (Limits.colimit G) Q ⟶ Z)
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι F j) Q)
(CategoryStruct.comp (whiskerRight (Limits.HasColimit.isoOfNatIso w).hom Q) h) = CategoryStruct.comp (whiskerRight (w.hom.app j) Q) (CategoryStruct.comp (whiskerRight (Limits.colimit.ι G j) Q) h)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.colimit.whiskerLeft_ι_desc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F : Functor J C}
[Limits.HasColimit F]
(c : Limits.Cocone F)
(j : J)
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q (Limits.colimit.ι F j)) (whiskerLeft Q (Limits.colimit.desc F c)) = whiskerLeft Q (c.ι.app j)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.colimit.whiskerLeft_ι_desc_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F : Functor J C}
[Limits.HasColimit F]
(c : Limits.Cocone F)
(j : J)
{Q Z : C}
(h : tensorObj Q c.pt ⟶ Z)
:
CategoryStruct.comp (whiskerLeft Q (Limits.colimit.ι F j))
(CategoryStruct.comp (whiskerLeft Q (Limits.colimit.desc F c)) h) = CategoryStruct.comp (whiskerLeft Q (c.ι.app j)) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.colimit.ι_desc_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F : Functor J C}
[Limits.HasColimit F]
(c : Limits.Cocone F)
(j : J)
{Q : C}
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι F j) Q) (whiskerRight (Limits.colimit.desc F c) Q) = whiskerRight (c.ι.app j) Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.colimit.ι_desc_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{F : Functor J C}
[Limits.HasColimit F]
(c : Limits.Cocone F)
(j : J)
{Q Z : C}
(h : tensorObj c.pt Q ⟶ Z)
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι F j) Q)
(CategoryStruct.comp (whiskerRight (Limits.colimit.desc F c) Q) h) = CategoryStruct.comp (whiskerRight (c.ι.app j) Q) h