Theorems · Theorem · category theory

CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff

∀ {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) [L.IsLocalization W] [L.CommShift M]
  (X Y : C),
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔
    ∀ (a b : M),
      Small.{w, v₂} ((CategoryTheory.shiftFunctor D a).obj (L.obj X) ⟶ (CategoryTheory.shiftFunctor D b).obj (L.obj Y))

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.CommShift