Theorems · Theorem · category theory

CategoryTheory.Localization.SmallShiftedHom.equiv_comp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y Z : C} [inst_7 : W.IsCompatibleWithShift M]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] {a b c : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (g : CategoryTheory.Localization.SmallShiftedHom W Y Z b)
  (h : b + a = c),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.comp g h) =
    ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f).comp
      ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) g) h

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.CommShiftCategoryTheory.MorphismProperty.IsCompatibleWithShiftCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHom