Theorems · Theorem · category theory

CategoryTheory.Localization.SmallShiftedHom.precompEquiv_symm_apply

∀ {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] {X Y Z : C} [inst_3 : W.RespectsIso]
  [inst_4 : W.IsCompatibleWithShift M] [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X]
  [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] (f : X ⟶ Y) (hf : W f) {a : M}
  (β : CategoryTheory.Localization.SmallShiftedHom W X Z a),
  (CategoryTheory.Localization.SmallShiftedHom.precompEquiv f hf).symm β =
    (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv 0 ⋯ f hf).comp β ⋯

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

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