Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.isVerdierRightLocalizing_iff

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms],
  A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y),
      A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp s b = s'

Defined in

Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.HasShiftCategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.PretriangulatedCategoryTheory.ObjectProperty.IsTriangulatedCategoryTheory.ObjectProperty.IsTriangulatedCategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms