Owner-authored Postnikov towers

This file begins the repository-owned foundation for Bridgeland stability. A PostnikovTower C E packages a finite filtration of E by distinguished triangles and depends only on Mathlib.

structure CategoryTheory.Triangulated.PostnikovTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (E : C) : Type (max u v)

A finite Postnikov tower of E. The i-th factor is the third object of the distinguished triangle connecting consecutive objects in the chain.

• n : ℕ

  The number of factors.

• chain : ComposableArrows C self.n

  The filtered chain A₀ ⟶ A₁ ⟶ ⋯ ⟶ Aₙ.

• triangle : Fin self.n → Pretriangulated.Triangle C

  The triangle connecting each consecutive pair.

• triangle_dist (i : Fin self.n) : self.triangle i ∈ Pretriangulated.distinguishedTriangles

  Every connecting triangle is distinguished.

• triangle_obj₁ (i : Fin self.n) : Nonempty ((self.triangle i).obj₁ ≅ self.chain.obj' ↑i ⋯)

  The first triangle object agrees with the lower chain object.

• triangle_obj₂ (i : Fin self.n) : Nonempty ((self.triangle i).obj₂ ≅ self.chain.obj' (↑i + 1) ⋯)

  The second triangle object agrees with the upper chain object.

• base_isZero : Limits.IsZero self.chain.left

  The tower begins at a zero object.

• top_iso : Nonempty (self.chain.right ≅ E)

  The top of the tower is isomorphic to the filtered object.

def CategoryTheory.Triangulated.PostnikovTower.length (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} (P : PostnikovTower C E) : ℕ

The number of factors in a Postnikov tower.

Equations

• CategoryTheory.Triangulated.PostnikovTower.length C P = P.n

theorem CategoryTheory.Triangulated.PostnikovTower.isZero_of_length_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} (P : PostnikovTower C E) (h : P.n = 0) : Limits.IsZero E

A tower with no factors filters only a zero object.

Formerly a structure field (zero_isZero), which overstated what a constructor must supply: a length-zero chain starts and ends at the same object, so base_isZero transported across top_iso already proves this.

def CategoryTheory.Triangulated.PostnikovTower.factor {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} (P : PostnikovTower C E) (i : Fin P.n) : C

The i-th factor of a Postnikov tower.

Equations

• P.factor i = (P.triangle i).obj₃

def CategoryTheory.Triangulated.PostnikovTower.factors {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} (P : PostnikovTower C E) : Fin P.n → C

The family of all factor objects of a Postnikov tower.

Equations

• P.factors = P.factor