16. Mathlib🔗

16.1. TStructure🔗

[Definition 3.1]

structure

CategoryTheory.Triangulated.TStructure.{v_1, u_1} (C : Type u_1)
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] : Type u_1
CategoryTheory.Triangulated.TStructure.{v_1,
    u_1}
  (C : Type u_1)
  [CategoryTheory.Category.{v_1, u_1} C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C] :
  Type u_1

Constructor

CategoryTheory.Triangulated.TStructure.mk.{v_1, u_1}

Fields

le : ℤ → CategoryTheory.ObjectProperty C

the predicate of objects that are ≤ n for n : ℤ.

ge : ℤ → CategoryTheory.ObjectProperty C

the predicate of objects that are ≥ n for n : ℤ.

le_isClosedUnderIsomorphisms : ∀ (n : ℤ), (self.le n).IsClosedUnderIsomorphisms

ge_isClosedUnderIsomorphisms : ∀ (n : ℤ), (self.ge n).IsClosedUnderIsomorphisms

le_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), self.le n X → self.le n' ((CategoryTheory.shiftFunctor C a).obj X)

ge_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), self.ge n X → self.ge n' ((CategoryTheory.shiftFunctor C a).obj X)

zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), self.le 0 X → self.ge 1 Y → f = 0

le_zero_le : self.le 0 ≤ self.le 1

ge_one_le : self.ge 1 ≤ self.ge 0

exists_triangle_zero_one : ∀ (A : C),
  ∃ X Y,
    ∃ (_ : self.le 0 X) (_ : self.ge 1 Y),
      ∃ f g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change