Theorems · Theorem · category theory

CategoryTheory.ShiftedHom.comp_assoc

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M} (α : CategoryTheory.ShiftedHom X Y a₁)
  (β : CategoryTheory.ShiftedHom Y Z a₂) (γ : CategoryTheory.ShiftedHom Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂)
  (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a), (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Defined in

Mathlib.CategoryTheory.Shift.ShiftedHom

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShift