Pullbacks and pushouts 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.HasLimits 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.IsPushout.whiskerLeft_inl_desc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q : C}
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_desc_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q Z✝ : C}
(h✝ : tensorObj Q W ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q inl) (CategoryStruct.comp (whiskerLeft Q (hP.desc h k w)) h✝) = CategoryStruct.comp (whiskerLeft Q h) h✝
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q : C}
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q Z✝ : C}
(h✝ : tensorObj Q W ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q inr) (CategoryStruct.comp (whiskerLeft Q (hP.desc h k w)) h✝) = CategoryStruct.comp (whiskerLeft Q k) h✝
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q : C}
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q Z✝ : C}
(h✝ : tensorObj W Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight inl Q) (CategoryStruct.comp (whiskerRight (hP.desc h k w) Q) h✝) = CategoryStruct.comp (whiskerRight h Q) h✝
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q : C}
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Q Z✝ : C}
(h✝ : tensorObj W Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight inr Q) (CategoryStruct.comp (whiskerRight (hP.desc h k w) Q) h✝) = CategoryStruct.comp (whiskerRight k Q) h✝
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q f) (whiskerLeft Q inl) = CategoryStruct.comp (whiskerLeft Q g) (whiskerLeft Q inr)
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{Q Z✝ : C}
(h : tensorObj Q P ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q f) (CategoryStruct.comp (whiskerLeft Q inl) h) = CategoryStruct.comp (whiskerLeft Q g) (CategoryStruct.comp (whiskerLeft Q inr) h)
theorem
CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{Q : C}
:
CategoryStruct.comp (whiskerRight f Q) (whiskerRight inl Q) = CategoryStruct.comp (whiskerRight g Q) (whiskerRight inr Q)
theorem
CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{Q Z✝ : C}
(h : tensorObj P Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight f Q) (CategoryStruct.comp (whiskerRight inl Q) h) = CategoryStruct.comp (whiskerRight g Q) (CategoryStruct.comp (whiskerRight inr Q) h)
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (whiskerLeft Q hP.isoPushout.inv) = whiskerLeft Q inl
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj Q P ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.inv) h) = CategoryStruct.comp (whiskerLeft Q inl) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (whiskerLeft Q hP.isoPushout.inv) = whiskerLeft Q inr
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj Q P ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.inv) h) = CategoryStruct.comp (whiskerLeft Q inr) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q inl) (whiskerLeft Q hP.isoPushout.hom) = whiskerLeft Q (Limits.pushout.inl f g)
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj Q (Limits.pushout f g) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q inl) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q inr) (whiskerLeft Q hP.isoPushout.hom) = whiskerLeft Q (Limits.pushout.inr f g)
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj Q (Limits.pushout f g) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q inr) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (whiskerRight hP.isoPushout.inv Q) = whiskerRight inl Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj P Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q)
(CategoryStruct.comp (whiskerRight hP.isoPushout.inv Q) h) = CategoryStruct.comp (whiskerRight inl Q) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (whiskerRight hP.isoPushout.inv Q) = whiskerRight inr Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj P Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q)
(CategoryStruct.comp (whiskerRight hP.isoPushout.inv Q) h) = CategoryStruct.comp (whiskerRight inr Q) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerRight inl Q) (whiskerRight hP.isoPushout.hom Q) = whiskerRight (Limits.pushout.inl f g) Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj (Limits.pushout f g) Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight inl Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q : C}
:
CategoryStruct.comp (whiskerRight inr Q) (whiskerRight hP.isoPushout.hom Q) = whiskerRight (Limits.pushout.inr f g) Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
[Limits.HasPushout f g]
{Q Z✝ : C}
(h : tensorObj (Limits.pushout f g) Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight inr Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) h
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{Q : C}
:
CategoryStruct.comp (whiskerLeft Q f) (whiskerLeft Q (Limits.pushout.inl f g)) = CategoryStruct.comp (whiskerLeft Q g) (whiskerLeft Q (Limits.pushout.inr f g))
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{Q Z✝ : C}
(h : tensorObj Q (Limits.pushout f g) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q f) (CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) h) = CategoryStruct.comp (whiskerLeft Q g) (CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) h)
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{Q : C}
:
CategoryStruct.comp (whiskerRight f Q) (whiskerRight (Limits.pushout.inl f g) Q) = CategoryStruct.comp (whiskerRight g Q) (whiskerRight (Limits.pushout.inr f g) Q)
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{Q Z✝ : C}
(h : tensorObj (Limits.pushout f g) Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight f Q) (CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) h) = CategoryStruct.comp (whiskerRight g Q) (CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) h)
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{A B X Y Z W : C}
{f : A ⟶ B}
{g : X ⟶ Y}
{h : tensorObj Z W ⟶ X}
:
CategoryStruct.comp (whiskerRight (whiskerRight f Z) W)
(CategoryStruct.comp (associator B Z W).hom
(CategoryStruct.comp (whiskerLeft B h) (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)))) = CategoryStruct.comp (associator A Z W).hom
(CategoryStruct.comp (whiskerLeft A (CategoryStruct.comp h g))
(Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)))
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{A B X Y Z W : C}
{f : A ⟶ B}
{g : X ⟶ Y}
{h : tensorObj Z W ⟶ X}
{Z✝ : C}
(h✝ : Limits.pushout (whiskerRight f X) (whiskerLeft A g) ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight (whiskerRight f Z) W)
(CategoryStruct.comp (associator B Z W).hom
(CategoryStruct.comp (whiskerLeft B h)
(CategoryStruct.comp (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)) h✝))) = CategoryStruct.comp (associator A Z W).hom
(CategoryStruct.comp (whiskerLeft A (CategoryStruct.comp h g))
(CategoryStruct.comp (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)) h✝))
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{A B X Y Z W : C}
{f : A ⟶ B}
{g : X ⟶ Y}
{h : tensorObj Z W ⟶ A}
:
CategoryStruct.comp (whiskerLeft Z (whiskerLeft W g))
(CategoryStruct.comp (associator Z W Y).inv
(CategoryStruct.comp (whiskerRight h Y) (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)))) = CategoryStruct.comp (associator Z W X).inv
(CategoryStruct.comp (whiskerRight (CategoryStruct.comp h f) X)
(Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)))
theorem
CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{A B X Y Z W : C}
{f : A ⟶ B}
{g : X ⟶ Y}
{h : tensorObj Z W ⟶ A}
{Z✝ : C}
(h✝ : Limits.pushout (whiskerRight f X) (whiskerLeft A g) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Z (whiskerLeft W g))
(CategoryStruct.comp (associator Z W Y).inv
(CategoryStruct.comp (whiskerRight h Y)
(CategoryStruct.comp (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)) h✝))) = CategoryStruct.comp (associator Z W X).inv
(CategoryStruct.comp (whiskerRight (CategoryStruct.comp h f) X)
(CategoryStruct.comp (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)) h✝))
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) = whiskerLeft Q (Limits.pushout.inr g f)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
{Z✝ : C}
(h : tensorObj Q (Limits.pushout g f) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g))
(CategoryStruct.comp (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr g f)) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) = whiskerLeft Q (Limits.pushout.inl g f)
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
{Z✝ : C}
(h : tensorObj Q (Limits.pushout g f) ⟶ Z✝)
:
CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g))
(CategoryStruct.comp (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl g f)) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (whiskerRight (Limits.pushoutSymmetry f g).hom Q) = whiskerRight (Limits.pushout.inr g f) Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
{Z✝ : C}
(h : tensorObj (Limits.pushout g f) Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q)
(CategoryStruct.comp (whiskerRight (Limits.pushoutSymmetry f g).hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inr g f) Q) h
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (whiskerRight (Limits.pushoutSymmetry f g).hom Q) = whiskerRight (Limits.pushout.inl g f) Q
@[simp]
theorem
CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight_assoc
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Limits.HasPushouts C]
{Q X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
{Z✝ : C}
(h : tensorObj (Limits.pushout g f) Q ⟶ Z✝)
:
CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q)
(CategoryStruct.comp (whiskerRight (Limits.pushoutSymmetry f g).hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inl g f) Q) h