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