Theorems · Theorem · category theory

CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target

∀ {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 : C) {Y : C} [W.IsCompatibleWithShift M] {Y' : C}
  (f : Y ⟶ Y'),
  W f →
    (CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔
      CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y')

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.MorphismProperty.IsCompatibleWithShift