Bridgeland Stability Conditions

9.6. Slicing: TStructure🔗

9.6.1. zero🔗

A 0-factor HN filtration on a zero object: the chain is the single-vertex composable arrow 0 \to 0, with no triangles and no phases.

Construction: Sets n = 0, the chain to the constant E, and all triangle/phase data to vacuous matches. The base and top isomorphisms are both the identity on E.

🔗def
CategoryTheory.Triangulated.HNFiltration.zero.{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} (E : C)
  (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.HNFiltration C P E
CategoryTheory.Triangulated.HNFiltration.zero.{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}
  (E : C)
  (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.HNFiltration
    C P E

Something wrong, better idea? Suggest a change

9.6.2. single🔗

A 1-factor HN filtration for a semistable object S \in \mathcal{P}(\phi): the chain is 0 \to S with the unique distinguished triangle 0 \to S \xrightarrow{\mathrm{id}} S \to 0.

Construction: Sets n = 1, the chain to the composable arrow 0 \to S, the single phase to \phi, and the single triangle to the contractible distinguished triangle on S. Strict antitonicity is vacuous for a singleton.

🔗def
CategoryTheory.Triangulated.HNFiltration.single.{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} (S : C) (φ : ℝ)
  (hS : P φ S) : CategoryTheory.Triangulated.HNFiltration C P S
CategoryTheory.Triangulated.HNFiltration.single.{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}
  (S : C) (φ : ℝ) (hS : P φ S) :
  CategoryTheory.Triangulated.HNFiltration
    C P S

Something wrong, better idea? Suggest a change

9.6.3. leProp_of_semistable🔗

A semistable object S \in \mathcal{P}(\phi) with \phi \le t satisfies \mathcal{P}(\le t).

Proof: Use the single-factor filtration; then \phi^+ = \phi \le t.

🔗theorem
CategoryTheory.Triangulated.Slicing.leProp_of_semistable.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (φ t : ℝ) (S : C)
  (hS : s.P φ S) (hle : φ ≤ t) :
  CategoryTheory.Triangulated.Slicing.leProp C s t S
CategoryTheory.Triangulated.Slicing.leProp_of_semistable.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (φ t : ℝ) (S : C) (hS : s.P φ S)
  (hle : φ ≤ t) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s t S

Something wrong, better idea? Suggest a change

9.6.4. gtProp_of_semistable🔗

A semistable object S \in \mathcal{P}(\phi) with \phi > t satisfies \mathcal{P}(> t).

Proof: Use the single-factor filtration; then \phi^- = \phi > t.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_of_semistable.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (φ t : ℝ) (S : C)
  (hS : s.P φ S) (hgt : t < φ) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t S
CategoryTheory.Triangulated.Slicing.gtProp_of_semistable.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (φ t : ℝ) (S : C) (hS : s.P φ S)
  (hgt : t < φ) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s t S

Something wrong, better idea? Suggest a change

9.6.5. phiPlus_eq_phiMinus_of_semistable🔗

For a semistable nonzero object E \in \mathcal{P}(\phi), \phi^+(E) = \phi^-(E) = \phi.

Proof: The single-factor filtration has \phi^+ = \phi^- = \phi, and the uniqueness theorems phiPlus_eq and phiMinus_eq identify the intrinsic values.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_eq_phiMinus_of_semistable.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C} {φ : ℝ}
  (hS : s.P φ E) (hE : ¬CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE = φ ∧
    CategoryTheory.Triangulated.Slicing.phiMinus C s E hE = φ
CategoryTheory.Triangulated.Slicing.phiPlus_eq_phiMinus_of_semistable.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C} {φ : ℝ} (hS : s.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE =
      φ ∧
    CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE =
      φ

Something wrong, better idea? Suggest a change

9.6.6. semistable_of_phiPlus_eq_phiMinus🔗

Converse. If \phi^+(E) = \phi^-(E) for a nonzero object E, then E is semistable of phase \phi^+(E).

Proof: Equal extreme phases combined with strict antitonicity of the phase sequence forces the filtration length n = 1. The single triangle then has a zero first vertex, making \mathrm{mor}_2 an isomorphism. Thus E is isomorphic to the unique factor, which is semistable of the claimed phase.

🔗theorem
CategoryTheory.Triangulated.Slicing.semistable_of_phiPlus_eq_phiMinus.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (heq :
    CategoryTheory.Triangulated.Slicing.phiPlus C s E hE =
      CategoryTheory.Triangulated.Slicing.phiMinus C s E hE) :
  s.P (CategoryTheory.Triangulated.Slicing.phiPlus C s E hE) E
CategoryTheory.Triangulated.Slicing.semistable_of_phiPlus_eq_phiMinus.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (heq :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE =
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE) :
  s.P
    (CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE)
    E

Something wrong, better idea? Suggest a change

9.6.7. semistable_of_triangle🔗

Extension-closure of \mathcal{P}(\phi). If A, B \in \mathcal{P}(\phi) and A \to E \to B \to A[1] is distinguished, then E \in \mathcal{P}(\phi).

Proof: Uses phiPlus_lt_of_triangle and phiMinus_gt_of_triangle to pin \phi^+(E) = \phi^-(E) = \phi, then invokes semistable_of_phiPlus_eq_phiMinus.

🔗theorem
CategoryTheory.Triangulated.Slicing.semistable_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]
  (s : CategoryTheory.Triangulated.Slicing C) {A E B : C} (φ : ℝ)
  (hA : s.P φ A) (hB : s.P φ B) {f : A ⟶ E} {g : E ⟶ B}
  {h : B ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  s.P φ E
CategoryTheory.Triangulated.Slicing.semistable_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {A E B : C} (φ : ℝ) (hA : s.P φ A)
  (hB : s.P φ B) {f : A ⟶ E} {g : E ⟶ B}
  {h :
    B ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  s.P φ E

Something wrong, better idea? Suggest a change

9.6.8. semistable_of_HN_all_eq🔗

If all factors in an HN filtration have the same phase \phi, then E is \mathcal{P}(\phi)-semistable.

Proof: Induction along the chain: at each step, the triangle has first vertex \mathcal{P}(\phi)-semistable (by the inductive hypothesis) and third vertex \mathcal{P}(\phi)-semistable (by hypothesis), so the middle vertex is \mathcal{P}(\phi)-semistable by semistable_of_triangle.

🔗theorem
CategoryTheory.Triangulated.Slicing.semistable_of_HN_all_eq.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C} {φ : ℝ}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hall : ∀ (i : Fin F.n), F.φ i = φ) : s.P φ E
CategoryTheory.Triangulated.Slicing.semistable_of_HN_all_eq.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C} {φ : ℝ}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hall : ∀ (i : Fin F.n), F.φ i = φ) :
  s.P φ E

Something wrong, better idea? Suggest a change

9.6.9. IsBounded🔗

A t-structure on a triangulated category is bounded if every object E lies between some integer levels: there exist a, b \in \mathbb{Z} with E \in \mathcal{D}^{\le a} \cap \mathcal{D}^{\ge b}.

Construction: A proposition asserting that for every object E, there exist integers a, b such that t.le a E and t.ge b E both hold.

🔗def
CategoryTheory.Triangulated.TStructure.IsBounded.{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]
  (t : CategoryTheory.Triangulated.TStructure C) : Prop
CategoryTheory.Triangulated.TStructure.IsBounded.{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]
  (t :
    CategoryTheory.Triangulated.TStructure
      C) :
  Prop

Something wrong, better idea? Suggest a change

9.6.10. zero_of_gtProp_leProp🔗

Any morphism from an object in \mathcal{P}(> 0) to an object in \mathcal{P}(\le 0) is zero.

Proof: Both objects have HN filtrations; the phase ranges create a gap (all source phases > 0 \ge all target phases), so hom_eq_zero_of_phase_gap applies.

🔗theorem
CategoryTheory.Triangulated.Slicing.zero_of_gtProp_leProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {X Y : C}
  (hX : CategoryTheory.Triangulated.Slicing.gtProp C s 0 X)
  (hY : CategoryTheory.Triangulated.Slicing.leProp C s 0 Y)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.Slicing.zero_of_gtProp_leProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y : C}
  (hX :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s 0 X)
  (hY :
    CategoryTheory.Triangulated.Slicing.leProp
      C s 0 Y)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.6.11. zero_of_geProp_ltProp🔗

Any morphism from an object in \mathcal{P}(\ge 0) to an object in \mathcal{P}(< 0) is zero.

Proof: Both objects have HN filtrations with a phase gap (source phases \ge 0 > target phases), so hom_eq_zero_of_phase_gap applies.

🔗theorem
CategoryTheory.Triangulated.Slicing.zero_of_geProp_ltProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) {X Y : C}
  (hX : CategoryTheory.Triangulated.Slicing.geProp C s 0 X)
  (hY : CategoryTheory.Triangulated.Slicing.ltProp C s 0 Y)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.Slicing.zero_of_geProp_ltProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {X Y : C}
  (hX :
    CategoryTheory.Triangulated.Slicing.geProp
      C s 0 X)
  (hY :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s 0 Y)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.6.12. HNFiltration.phaseShift🔗

Convert an HN filtration with respect to \mathcal{P} into one with respect to the shifted predicate \psi \mapsto \mathcal{P}(\psi + t), by subtracting t from all phases.

Construction: Preserves the chain, triangles, and semistability data. The new phase assignment is \phi_i - t, and strict antitonicity is preserved since subtracting a constant preserves order.

🔗def
CategoryTheory.Triangulated.HNFiltration.phaseShift.{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]
  {s : CategoryTheory.Triangulated.Slicing C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (t : ℝ) :
  CategoryTheory.Triangulated.HNFiltration C (fun ψ => s.P (ψ + t)) E
CategoryTheory.Triangulated.HNFiltration.phaseShift.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (t : ℝ) :
  CategoryTheory.Triangulated.HNFiltration
    C (fun ψ => s.P (ψ + t)) E

Something wrong, better idea? Suggest a change

9.6.13. Slicing.phaseShift🔗

The phase-shifted slicing \mathcal{P}_t defined by \mathcal{P}_t(\psi) = \mathcal{P}(\psi + t). This shifts all phases down by t.

Construction: Constructs a new Slicing by composing the predicate with addition by t. Shift compatibility, Hom-vanishing, and HN existence are verified by reducing to the corresponding properties of the original slicing.

🔗def
CategoryTheory.Triangulated.Slicing.phaseShift.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) :
  CategoryTheory.Triangulated.Slicing C
CategoryTheory.Triangulated.Slicing.phaseShift.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) :
  CategoryTheory.Triangulated.Slicing C

Something wrong, better idea? Suggest a change

9.6.14. phaseShift_gtProp_zero🔗

\mathcal{P}_t(> 0) coincides with \mathcal{P}(> t): an object has all shifted phases > 0 iff all original phases are > t.

Proof: Both directions convert between HN filtrations with shifted and unshifted phases by adding or subtracting t.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_gtProp_zero.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.gtProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) 0 E ↔
    CategoryTheory.Triangulated.Slicing.gtProp C s t E
CategoryTheory.Triangulated.Slicing.phaseShift_gtProp_zero.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.gtProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      0 E ↔
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t E

Something wrong, better idea? Suggest a change

9.6.15. phaseShift_gtProp🔗

\mathcal{P}_t(> u) coincides with \mathcal{P}(> u + t).

Proof: Generalization of phaseShift_gtProp_zero with parameter u.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_gtProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.gtProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) u E ↔
    CategoryTheory.Triangulated.Slicing.gtProp C s (u + t) E
CategoryTheory.Triangulated.Slicing.phaseShift_gtProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.gtProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      u E ↔
    CategoryTheory.Triangulated.Slicing.gtProp
      C s (u + t) E

Something wrong, better idea? Suggest a change

9.6.16. phaseShift_leProp_zero🔗

\mathcal{P}_t(\le 0) coincides with \mathcal{P}(\le t).

Proof: Both directions convert between shifted and unshifted filtrations.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_leProp_zero.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.leProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) 0 E ↔
    CategoryTheory.Triangulated.Slicing.leProp C s t E
CategoryTheory.Triangulated.Slicing.phaseShift_leProp_zero.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.leProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      0 E ↔
    CategoryTheory.Triangulated.Slicing.leProp
      C s t E

Something wrong, better idea? Suggest a change

9.6.17. phaseShift_leProp🔗

\mathcal{P}_t(\le u) coincides with \mathcal{P}(\le u + t).

Proof: Generalization of phaseShift_leProp_zero with parameter u.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_leProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.leProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) u E ↔
    CategoryTheory.Triangulated.Slicing.leProp C s (u + t) E
CategoryTheory.Triangulated.Slicing.phaseShift_leProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.leProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      u E ↔
    CategoryTheory.Triangulated.Slicing.leProp
      C s (u + t) E

Something wrong, better idea? Suggest a change

9.6.18. phaseShift_ltProp_zero🔗

\mathcal{P}_t(< 0) coincides with \mathcal{P}(< t).

Proof: Both directions convert between shifted and unshifted filtrations.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_ltProp_zero.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.ltProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) 0 E ↔
    CategoryTheory.Triangulated.Slicing.ltProp C s t E
CategoryTheory.Triangulated.Slicing.phaseShift_ltProp_zero.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.ltProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      0 E ↔
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t E

Something wrong, better idea? Suggest a change

9.6.19. phaseShift_ltProp🔗

\mathcal{P}_t(< u) coincides with \mathcal{P}(< u + t).

Proof: Generalization of phaseShift_ltProp_zero with parameter u.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_ltProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.ltProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) u E ↔
    CategoryTheory.Triangulated.Slicing.ltProp C s (u + t) E
CategoryTheory.Triangulated.Slicing.phaseShift_ltProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.ltProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      u E ↔
    CategoryTheory.Triangulated.Slicing.ltProp
      C s (u + t) E

Something wrong, better idea? Suggest a change

9.6.20. phaseShift_geProp_zero🔗

\mathcal{P}_t(\ge 0) coincides with \mathcal{P}(\ge t).

Proof: Both directions convert between shifted and unshifted filtrations.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_geProp_zero.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.geProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) 0 E ↔
    CategoryTheory.Triangulated.Slicing.geProp C s t E
CategoryTheory.Triangulated.Slicing.phaseShift_geProp_zero.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.geProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      0 E ↔
    CategoryTheory.Triangulated.Slicing.geProp
      C s t E

Something wrong, better idea? Suggest a change

9.6.21. phaseShift_geProp🔗

\mathcal{P}_t(\ge u) coincides with \mathcal{P}(\ge u + t).

Proof: Generalization of phaseShift_geProp_zero with parameter u.

🔗theorem
CategoryTheory.Triangulated.Slicing.phaseShift_geProp.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.geProp C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t) u E ↔
    CategoryTheory.Triangulated.Slicing.geProp C s (u + t) E
CategoryTheory.Triangulated.Slicing.phaseShift_geProp.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t u : ℝ) (E : C) :
  CategoryTheory.Triangulated.Slicing.geProp
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C s t)
      u E ↔
    CategoryTheory.Triangulated.Slicing.geProp
      C s (u + t) E

Something wrong, better idea? Suggest a change

9.6.22. zero_of_gtProp_leProp_general🔗

For any cutoff t \in \mathbb{R}, any morphism from \mathcal{P}(> t) to \mathcal{P}(\le t) is zero.

Proof: Reduce to the t = 0 case via phaseShift: apply zero_of_gtProp_leProp to the phase-shifted slicing.

🔗theorem
CategoryTheory.Triangulated.Slicing.zero_of_gtProp_leProp_general.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) {X Y : C}
  (hX : CategoryTheory.Triangulated.Slicing.gtProp C s t X)
  (hY : CategoryTheory.Triangulated.Slicing.leProp C s t Y)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.Slicing.zero_of_gtProp_leProp_general.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) {X Y : C}
  (hX :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t X)
  (hY :
    CategoryTheory.Triangulated.Slicing.leProp
      C s t Y)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.6.23. zero_of_geProp_ltProp_general🔗

For any cutoff t \in \mathbb{R}, any morphism from \mathcal{P}(\ge t) to \mathcal{P}(< t) is zero.

Proof: Reduce to the t = 0 case via phaseShift: apply zero_of_geProp_ltProp to the phase-shifted slicing.

🔗theorem
CategoryTheory.Triangulated.Slicing.zero_of_geProp_ltProp_general.{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]
  (s : CategoryTheory.Triangulated.Slicing C) (t : ℝ) {X Y : C}
  (hX : CategoryTheory.Triangulated.Slicing.geProp C s t X)
  (hY : CategoryTheory.Triangulated.Slicing.ltProp C s t Y)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.Slicing.zero_of_geProp_ltProp_general.{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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (t : ℝ) {X Y : C}
  (hX :
    CategoryTheory.Triangulated.Slicing.geProp
      C s t X)
  (hY :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t Y)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.6.24. unphaseShift🔗

Convert an HN filtration with respect to the shifted slicing (\mathcal{P}_t) back to one with respect to \mathcal{P}, by adding t to all phases. Inverse of phaseShift.

Construction: Preserves the chain and triangle data. The new phase assignment is \phi_i + t.

🔗def
CategoryTheory.Triangulated.HNFiltration.unphaseShift.{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]
  {s : CategoryTheory.Triangulated.Slicing C} {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t).P E) :
  CategoryTheory.Triangulated.HNFiltration C s.P E
CategoryTheory.Triangulated.HNFiltration.unphaseShift.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
          C s t).P
      E) :
  CategoryTheory.Triangulated.HNFiltration
    C s.P E

Something wrong, better idea? Suggest a change

9.6.25. unphaseShift_n🔗

The filtration length is preserved by unphaseShift.

Proof: By definition (rfl).

🔗theorem
CategoryTheory.Triangulated.HNFiltration.unphaseShift_n.{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]
  {s : CategoryTheory.Triangulated.Slicing C} {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t).P E) :
  (CategoryTheory.Triangulated.HNFiltration.unphaseShift C G).n = G.n
CategoryTheory.Triangulated.HNFiltration.unphaseShift_n.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
          C s t).P
      E) :
  (CategoryTheory.Triangulated.HNFiltration.unphaseShift
        C G).n =
    G.n

Something wrong, better idea? Suggest a change

9.6.26. unphaseShift_phiPlus🔗

The highest phase of the unshifted filtration equals the shifted highest phase plus t: \phi^+(\mathrm{unphaseShift}(G)) = \phi^+(G) + t.

Proof: By definition (rfl).

🔗theorem
CategoryTheory.Triangulated.HNFiltration.unphaseShift_phiPlus.{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]
  {s : CategoryTheory.Triangulated.Slicing C} {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration C
      (CategoryTheory.Triangulated.Slicing.phaseShift C s t).P E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus C
      (CategoryTheory.Triangulated.HNFiltration.unphaseShift C G) hn =
    CategoryTheory.Triangulated.HNFiltration.phiPlus C G hn + t
CategoryTheory.Triangulated.HNFiltration.unphaseShift_phiPlus.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {E : C} {t : ℝ}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
          C s t).P
      E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus
      C
      (CategoryTheory.Triangulated.HNFiltration.unphaseShift
        C G)
      hn =
    CategoryTheory.Triangulated.HNFiltration.phiPlus
        C G hn +
      t

Something wrong, better idea? Suggest a change