5. PostnikovTower.Defs
Module BridgelandStability.PostnikovTower.Defs — 2 declarations (Structure, Definition)
5.1. CategoryTheory.Triangulated.PostnikovTower
Structure | BridgelandStability.PostnikovTower.Defs | Source | Open Issue
/-- A Postnikov tower of an object `E` in a pretriangulated category. This consists of
a chain of `n+1` objects connected by `n` distinguished triangles:
```
0 = A₀ → A₁ → ⋯ → Aₙ ≅ E
```
where each step `Aᵢ → Aᵢ₊₁` completes to a distinguished triangle
`Aᵢ → Aᵢ₊₁ → Fᵢ → Aᵢ⟦1⟧` with factor `Fᵢ = (triangle i).obj₃`.
The factor objects are derived from the triangles (as `obj₃`) rather than stored
as a separate data field. -/
structure PostnikovTower (E : C) where
/-- The number of factors (equivalently, the number of distinguished triangles). -/
n : ℕ
/-- The chain of objects: `A₀ → A₁ → ⋯ → Aₙ`. -/
chain : ComposableArrows C n
/-- Each consecutive pair of objects completes to a distinguished triangle. -/
triangle : Fin n → Pretriangulated.Triangle C
/-- Each triangle is distinguished. -/
triangle_dist : ∀ i, triangle i ∈ distTriang C
/-- The triangle's first object is isomorphic to the i-th chain object. -/
triangle_obj₁ : ∀ i, Nonempty ((triangle i).obj₁ ≅ chain.obj' i.val (C:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated CE:Cn:ℕchain:ComposableArrows C ntriangle:Fin n → Triangle Ctriangle_dist:∀ (i : Fin n), triangle i ∈ distinguishedTrianglesi:Fin n⊢ ↑i ≤ n All goals completed! 🐙))
/-- The triangle's second object is isomorphic to the (i+1)-th chain object. -/
triangle_obj₂ : ∀ i, Nonempty ((triangle i).obj₂ ≅ chain.obj' (i.val + 1) (C:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated CE:Cn:ℕchain:ComposableArrows C ntriangle:Fin n → Triangle Ctriangle_dist:∀ (i : Fin n), triangle i ∈ distinguishedTrianglestriangle_obj₁:∀ (i : Fin n), Nonempty ((triangle i).obj₁ ≅ chain.obj' ↑i ⋯)i:Fin n⊢ ↑i + 1 ≤ n All goals completed! 🐙))
/-- The leftmost object is zero. -/
base_isZero : IsZero (chain.left)
/-- The rightmost object is isomorphic to `E`. -/
top_iso : Nonempty (chain.right ≅ E)
/-- When `n = 0`, the object `E` is zero. -/
zero_isZero : n = 0 → IsZero E
5.2. CategoryTheory.Triangulated.PostnikovTower.factor
Definition | BridgelandStability.PostnikovTower.Defs | Source | Open Issue
/-- The `i`-th factor of a Postnikov tower, derived as `obj₃` of the `i`-th
distinguished triangle. -/
def PostnikovTower.factor {E : C} (P : PostnikovTower C E) (i : Fin P.n) : C :=
(P.triangle i).obj₃