Theorems · Theorem · category theory

CategoryTheory.Localization.SmallShiftedHom.comp_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y Z T : C}
  {a₁ a₂ a₃ a₁₂ a₂₃ a : M} [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X T]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y T]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z T]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M T T]
  (α : CategoryTheory.Localization.SmallShiftedHom W X Y a₁) (β : CategoryTheory.Localization.SmallShiftedHom W Y Z a₂)
  (γ : CategoryTheory.Localization.SmallShiftedHom W 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.Localization.SmallShiftedHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.MorphismProperty.IsCompatibleWithShiftCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHom