1. PostnikovTower🔗

1.1. PostnikovTower🔗

A Postnikov tower of an object E in a pretriangulated category \mathcal{C} is a finite filtration 0 = A_0 \to A_1 \to \cdots \to A_n \cong E where each step A_i \to A_{i+1} completes to a distinguished triangle A_i \to A_{i+1} \to F_i \to A_i[1]. The factor objects F_i are derived as the third vertices of these triangles. This separates the tower/filtration data from any phase or semistability data that may be layered on top (e.g., for Harder--Narasimhan filtrations).

Construction: A structure carrying: the length n; a ComposableArrows C n chain of objects; a family of distinguished triangles indexed by \operatorname{Fin}\, n; isomorphisms identifying each triangle's first and second vertices with consecutive chain objects; a proof that the base A_0 is zero; a proof that the top A_n \cong E; and a degeneracy proof that E is zero when n = 0.

structure

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

0 = A₀ → A₁ → ⋯ → Aₙ ≅ E

Constructor

CategoryTheory.Triangulated.PostnikovTower.mk.{v, u}

Fields

n : ℕ

The number of factors (equivalently, the number of distinguished triangles).

chain : CategoryTheory.ComposableArrows C self.n

The chain of objects: A₀ → A₁ → ⋯ → Aₙ.

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

Each consecutive pair of objects completes to a distinguished triangle.

triangle_dist : ∀ (i : Fin self.n), self.triangle i ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Each triangle is distinguished.

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

The triangle's first object is isomorphic to the i-th chain object.

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

The triangle's second object is isomorphic to the (i+1)-th chain object.

base_isZero : CategoryTheory.Limits.IsZero self.chain.left

The leftmost object is zero.

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

The rightmost object is isomorphic to E.

zero_isZero : self.n = 0 → CategoryTheory.Limits.IsZero E

When n = 0, the object E is zero.

Something wrong, better idea? Suggest a change

1.2. length🔗

The length of a Postnikov tower, equal to the number of factors n.

Construction: Returns the field P.n.

def

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

Something wrong, better idea? Suggest a change

1.3. factor🔗

The i-th factor of a Postnikov tower, defined as the third vertex (P.\operatorname{triangle}\, i).\operatorname{obj}_3 of the i-th distinguished triangle.

Construction: Defined as (P.triangle i).obj_3, extracting the factor directly from the triangle data without a separate stored field.

def

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

Something wrong, better idea? Suggest a change

1.4. factors🔗

The sequence of all factor objects of a Postnikov tower, as a function \operatorname{Fin}\, n \to \mathcal{C}.

Construction: Defined as P.factor, repackaging the factor function.

def

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

Something wrong, better idea? Suggest a change