Theorems · Theorem · category theory

CategoryTheory.NatTrans.CommShift.verticalComposition

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₁₃ : CategoryTheory.Functor C₁ C₃}
  (α : F₁₃ ⟶ F₁₂.comp F₂₃) {G₁₂ : CategoryTheory.Functor D₁ D₂} {G₂₃ : CategoryTheory.Functor D₂ D₃}
  {G₁₃ : CategoryTheory.Functor D₁ D₃} (β : G₁₂.comp G₂₃ ⟶ G₁₃) {L₁ : CategoryTheory.Functor C₁ D₁}
  {L₂ : CategoryTheory.Functor C₂ D₂} {L₃ : CategoryTheory.Functor C₃ D₃} (e₁₂ : F₁₂.comp L₂ ⟶ L₁.comp G₁₂)
  (e₂₃ : F₂₃.comp L₃ ⟶ L₂.comp G₂₃) (e₁₃ : F₁₃.comp L₃ ⟶ L₁.comp G₁₃) (A : Type u_7) [inst_6 : AddMonoid A]
  [inst_7 : CategoryTheory.HasShift C₁ A] [inst_8 : CategoryTheory.HasShift C₂ A]
  [inst_9 : CategoryTheory.HasShift C₃ A] [inst_10 : CategoryTheory.HasShift D₁ A]
  [inst_11 : CategoryTheory.HasShift D₂ A] [inst_12 : CategoryTheory.HasShift D₃ A] [inst_13 : F₁₂.CommShift A]
  [inst_14 : F₂₃.CommShift A] [inst_15 : F₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift α A]
  [inst_17 : G₁₂.CommShift A] [inst_18 : G₂₃.CommShift A] [inst_19 : G₁₃.CommShift A]
  [CategoryTheory.NatTrans.CommShift β A] [inst_21 : L₁.CommShift A] [inst_22 : L₂.CommShift A]
  [inst_23 : L₃.CommShift A] [CategoryTheory.NatTrans.CommShift e₁₂ A] [CategoryTheory.NatTrans.CommShift e₂₃ A],
  e₁₃ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α L₃)
        (CategoryTheory.CategoryStruct.comp ⋯ ⋯) →
    CategoryTheory.NatTrans.CommShift e₁₃ A

Assume that we have a diagram of categories `` C₁ ⥤ D₁ ‖ ‖ v v C₂ ⥤ D₂ ‖ ‖ v v C₃ ⥤ D₃ ` with functors F₁₂ : C₁ ⥤ C₂, F₂₃ : C₂ ⥤ C₃ and F₁₃ : C₁ ⥤ C₃ on the first column that are related by a natural transformation α : F₁₃ ⟶ F₁₂ ⋙ F₂₃ and similarly β : G₁₂ ⋙ G₂₃ ⟶ G₁₃ on the second column. Assume that we have natural transformations e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂ (top square), e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃ (bottom square), and e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃ (outer square), where the horizontal functors are denoted L₁, L₂ and L₃. Assume that e₁₃ is determined by the other natural transformations α, e₂₃, e₁₂ and β. Then, if all these categories are equipped with a shift by an additive monoid A, and all these functors commute with these shifts, then the natural transformation e₁₃ of the outer square commutes with the shift if all α, e₂₃, e₁₂ and β` do.

Defined in

Mathlib.CategoryTheory.Shift.CommShift

Cited by

0 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.NatTrans.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.NatTrans.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.NatTrans.CommShiftCategoryTheory.NatTrans.CommShift