Theorems · Definition · category theory

CategoryTheory.ObjectProperty.triangEnvelope

{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.ObjectProperty C

All objects that can be reached by shifts, binary products, retracts and extensions from objects in P. This is the smallest triangulated object property closed under retracts that contains P, see ObjectProperty.triangEnvelope_le_iff.

Defined in

Mathlib.CategoryTheory.Triangulated.Generators

Cited by

6 results in Mathlib

Foundations

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

Assumes

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