Theorems · Definition · category theory

CategoryTheory.ObjectProperty.trW

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 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] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C

Given P : ObjectProperty C with C a pretriangulated category, this is the class of morphisms whose cone satisfies P. (The name trW contains the prefix tr for "triangulated", and W is a letter that is often used to refer to classes of morphisms with respect to which we may consider the localized category.)

Defined in

Mathlib.CategoryTheory.Triangulated.Subcategory

Cited by

32 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.HasShiftCategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.Pretriangulated