14.8. Deformation: HNFiltrationAssembly🔗

14.8.1. semistable_of_hn_length_one🔗

An HN filtration of length one certifies that the object is semistable: if G is an HN filtration of Y with n = 1, then Y \in \mathcal{P}(\phi_0). The single distinguished triangle 0 \to E_1 \to F_0 with E_0 = 0 gives E_1 \cong F_0 and E_1 \cong Y (via the top isomorphism), so Y \cong F_0 \in \mathcal{P}(\phi_0).

Proof: The zeroth triangle has T.\mathrm{obj}_1 \cong 0 (base), so T.\mathrm{mor}_2 is an isomorphism. Compose with the top isomorphism to get F_0 \cong Y, then transport the semistability through the isomorphism.

theorem

CategoryTheory.Triangulated.semistable_of_hn_length_one.{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]
  {P : ℝ → CategoryTheory.ObjectProperty C}
  (hPiso : ∀ (φ : ℝ), (P φ).IsClosedUnderIsomorphisms) {Y : C}
  (GY : CategoryTheory.Triangulated.HNFiltration C P Y)
  (h1 : GY.n = 1) : P (GY.φ ⟨0, ⋯⟩) Y
CategoryTheory.Triangulated.semistable_of_hn_length_one.{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]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  (hPiso :
    ∀ (φ : ℝ),
      (P φ).IsClosedUnderIsomorphisms)
  {Y : C}
  (GY :
    CategoryTheory.Triangulated.HNFiltration
      C P Y)
  (h1 : GY.n = 1) : P (GY.φ ⟨0, ⋯⟩) Y

Something wrong, better idea? Suggest a change

14.8.2. append_hn_filtration_of_triangle🔗

Concatenate HN filtrations across a distinguished triangle X \to E \to Y \to X[1]: given filtrations G_X of X and G_Y of Y with all phases of G_Y strictly less than all phases of G_X, produce a filtration G of E whose phases are all > t. This is the generic Postnikov-splicing step for assembling the faithful S7 HN filtration from filtrations on successive \sigma-semistable factors.

Proof: Induction on the length of G_Y. Base: Y = 0 implies X \cong E, transport G_X. Inductive step: if n(G_Y) = 1, use appendFactor directly. Otherwise, peel off the last factor of G_Y via an octahedral axiom construction, recurse on the prefix, then append the last factor.

theorem

CategoryTheory.Triangulated.append_hn_filtration_of_triangle.{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] [CategoryTheory.IsTriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {X E Y : C}
  (hPiso : ∀ (φ : ℝ), (P φ).IsClosedUnderIsomorphisms)
  (GX : CategoryTheory.Triangulated.HNFiltration C P X)
  (GY : CategoryTheory.Triangulated.HNFiltration C P Y) (f : X ⟶ E)
  (g : E ⟶ Y) (h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (t : ℝ) (hX_gt : ∀ (j : Fin GX.n), t < GX.φ j)
  (hY_gt : ∀ (i : Fin GY.n), t < GY.φ i)
  (hsep : ∀ (i : Fin GY.n) (j : Fin GX.n), GY.φ i < GX.φ j) :
  ∃ G, ∀ (j : Fin G.n), t < G.φ j
CategoryTheory.Triangulated.append_hn_filtration_of_triangle.{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]
  [CategoryTheory.IsTriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {X E Y : C}
  (hPiso :
    ∀ (φ : ℝ),
      (P φ).IsClosedUnderIsomorphisms)
  (GX :
    CategoryTheory.Triangulated.HNFiltration
      C P X)
  (GY :
    CategoryTheory.Triangulated.HNFiltration
      C P Y)
  (f : X ⟶ E) (g : E ⟶ Y)
  (h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (t : ℝ)
  (hX_gt : ∀ (j : Fin GX.n), t < GX.φ j)
  (hY_gt : ∀ (i : Fin GY.n), t < GY.φ i)
  (hsep :
    ∀ (i : Fin GY.n) (j : Fin GX.n),
      GY.φ i < GX.φ j) :
  ∃ G, ∀ (j : Fin G.n), t < G.φ j

Something wrong, better idea? Suggest a change

14.8.3. append_hn_filtration_of_triangle_le🔗

Upper-bound companion for append_hn_filtration_of_triangle: if all input phases of G_X and G_Y are \le U, then all output phases of G are also \le U. Follows from the phase structure of appendFactor.

Proof: Same induction as append_hn_filtration_of_triangle, additionally tracking the upper bound U through each recursive call. The appendFactor construction preserves the upper bound since it assigns phases from the input filtrations.

theorem

CategoryTheory.Triangulated.append_hn_filtration_of_triangle_le.{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] [CategoryTheory.IsTriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {X E Y : C}
  (hPiso : ∀ (φ : ℝ), (P φ).IsClosedUnderIsomorphisms)
  (GX : CategoryTheory.Triangulated.HNFiltration C P X)
  (GY : CategoryTheory.Triangulated.HNFiltration C P Y) (f : X ⟶ E)
  (g : E ⟶ Y) (h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (t U : ℝ) (hX_gt : ∀ (j : Fin GX.n), t < GX.φ j)
  (hY_gt : ∀ (i : Fin GY.n), t < GY.φ i)
  (hsep : ∀ (i : Fin GY.n) (j : Fin GX.n), GY.φ i < GX.φ j)
  (hX_le : ∀ (j : Fin GX.n), GX.φ j ≤ U)
  (hY_le : ∀ (i : Fin GY.n), GY.φ i ≤ U) :
  ∃ G, (∀ (j : Fin G.n), t < G.φ j) ∧ ∀ (j : Fin G.n), G.φ j ≤ U
CategoryTheory.Triangulated.append_hn_filtration_of_triangle_le.{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]
  [CategoryTheory.IsTriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {X E Y : C}
  (hPiso :
    ∀ (φ : ℝ),
      (P φ).IsClosedUnderIsomorphisms)
  (GX :
    CategoryTheory.Triangulated.HNFiltration
      C P X)
  (GY :
    CategoryTheory.Triangulated.HNFiltration
      C P Y)
  (f : X ⟶ E) (g : E ⟶ Y)
  (h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (t U : ℝ)
  (hX_gt : ∀ (j : Fin GX.n), t < GX.φ j)
  (hY_gt : ∀ (i : Fin GY.n), t < GY.φ i)
  (hsep :
    ∀ (i : Fin GY.n) (j : Fin GX.n),
      GY.φ i < GX.φ j)
  (hX_le : ∀ (j : Fin GX.n), GX.φ j ≤ U)
  (hY_le : ∀ (i : Fin GY.n), GY.φ i ≤ U) :
  ∃ G,
    (∀ (j : Fin G.n), t < G.φ j) ∧
      ∀ (j : Fin G.n), G.φ j ≤ U

Something wrong, better idea? Suggest a change

14.8.4. split_hn_filtration_at_cutoff🔗

Split an HN filtration F of A at an arbitrary cutoff t: there exist objects X, Y with filtrations G_X, G_Y, a distinguished triangle X \to A \to Y \to X[1], with all phases of G_X strictly > t and all phases of G_Y at most t. The Y-part phases are bounded below by the last phase of F, and G_X phases are a subset of F phases.

Proof: Induction on the length of F. Base: n = 0 gives trivial splits. Inductive step: if the last phase \phi_{n-1} > t, the entire filtration goes to X. If n = 1 and \phi_0 \le t, everything goes to Y. Otherwise, recurse on the prefix of F (dropping the last factor), then re-attach the last factor via the distinguished triangle from the original filtration.

theorem

CategoryTheory.Triangulated.split_hn_filtration_at_cutoff.{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] [CategoryTheory.IsTriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {A : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P A) (t : ℝ) :
  ∃ X Y GX GY f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      (∀ (j : Fin GX.n), t < GX.φ j) ∧
        (∀ (j : Fin GY.n), GY.φ j ≤ t) ∧
          (∀ (x : 0 < F.n) (j : Fin GY.n), F.φ ⟨F.n - 1, ⋯⟩ ≤ GY.φ j) ∧
            ∀ (j : Fin GX.n), ∃ i, GX.φ j = F.φ i
CategoryTheory.Triangulated.split_hn_filtration_at_cutoff.{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]
  [CategoryTheory.IsTriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {A : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P A)
  (t : ℝ) :
  ∃ X Y GX GY f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      (∀ (j : Fin GX.n), t < GX.φ j) ∧
        (∀ (j : Fin GY.n), GY.φ j ≤ t) ∧
          (∀ (x : 0 < F.n) (j : Fin GY.n),
              F.φ ⟨F.n - 1, ⋯⟩ ≤ GY.φ j) ∧
            ∀ (j : Fin GX.n),
              ∃ i, GX.φ j = F.φ i

Something wrong, better idea? Suggest a change