Bridgeland Stability Conditions

9.5. Slicing: Phase🔗

9.5.1. gtProp_shift🔗

If E \in \mathcal{P}(> t), then E[a] \in \mathcal{P}(> t + a) for any integer shift a.

Proof: Shift the HN filtration by a using shiftHN; the shifted lowest phase becomes \phi^- + a > t + a.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_shift.{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) (a : ℤ)
  (h : CategoryTheory.Triangulated.Slicing.gtProp C s t E) :
  CategoryTheory.Triangulated.Slicing.gtProp C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj E)
CategoryTheory.Triangulated.Slicing.gtProp_shift.{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) (a : ℤ)
  (h :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj
      E)

Something wrong, better idea? Suggest a change

9.5.2. leProp_shift🔗

If E \in \mathcal{P}(\le t), then E[a] \in \mathcal{P}(\le t + a) for any integer shift a.

Proof: Shift the HN filtration by a; the shifted highest phase becomes \phi^+ + a \le t + a.

🔗theorem
CategoryTheory.Triangulated.Slicing.leProp_shift.{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) (a : ℤ)
  (h : CategoryTheory.Triangulated.Slicing.leProp C s t E) :
  CategoryTheory.Triangulated.Slicing.leProp C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj E)
CategoryTheory.Triangulated.Slicing.leProp_shift.{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) (a : ℤ)
  (h :
    CategoryTheory.Triangulated.Slicing.leProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj
      E)

Something wrong, better idea? Suggest a change

9.5.3. ltProp_shift🔗

If E \in \mathcal{P}(< t), then E[a] \in \mathcal{P}(< t + a) for any integer shift a.

Proof: Shift the HN filtration by a; the shifted highest phase becomes \phi^+ + a < t + a.

🔗theorem
CategoryTheory.Triangulated.Slicing.ltProp_shift.{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) (a : ℤ)
  (h : CategoryTheory.Triangulated.Slicing.ltProp C s t E) :
  CategoryTheory.Triangulated.Slicing.ltProp C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj E)
CategoryTheory.Triangulated.Slicing.ltProp_shift.{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) (a : ℤ)
  (h :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj
      E)

Something wrong, better idea? Suggest a change

9.5.4. geProp_shift🔗

If E \in \mathcal{P}(\ge t), then E[a] \in \mathcal{P}(\ge t + a) for any integer shift a.

Proof: Shift the HN filtration by a; the shifted lowest phase becomes \phi^- + a \ge t + a.

🔗theorem
CategoryTheory.Triangulated.Slicing.geProp_shift.{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) (a : ℤ)
  (h : CategoryTheory.Triangulated.Slicing.geProp C s t E) :
  CategoryTheory.Triangulated.Slicing.geProp C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj E)
CategoryTheory.Triangulated.Slicing.geProp_shift.{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) (a : ℤ)
  (h :
    CategoryTheory.Triangulated.Slicing.geProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.geProp
    C s (t + ↑a)
    ((CategoryTheory.shiftFunctor C a).obj
      E)

Something wrong, better idea? Suggest a change

9.5.5. chain_hom_eq_zero_of_factor_zero🔗

If all morphisms from the first semistable factor A_1 of an HN filtration to E are zero, then all morphisms from A_1 to any chain object E_k are zero.

Proof: Downward induction starting from k = n (where E_n \cong E and the hypothesis applies directly). At each step, the coYoneda exact sequence on the inverse rotation of the k-th triangle, combined with Hom-vanishing on the shifted factor A_k[-1], extends the vanishing to E_k.

🔗theorem
CategoryTheory.Triangulated.chain_hom_eq_zero_of_factor_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) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (hn : 0 < F.n)
  (hzero : ∀ (f : (F.triangle ⟨0, hn⟩).obj₃ ⟶ E), f = 0) (k : ℕ)
  (hk : k < F.n + 1)
  (f : (F.triangle ⟨0, hn⟩).obj₃ ⟶ F.chain.obj ⟨k, hk⟩) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_of_factor_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)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < F.n)
  (hzero :
    ∀ (f : (F.triangle ⟨0, hn⟩).obj₃ ⟶ E),
      f = 0)
  (k : ℕ) (hk : k < F.n + 1)
  (f :
    (F.triangle ⟨0, hn⟩).obj₃ ⟶
      F.chain.obj ⟨k, hk⟩) :
  f = 0

Something wrong, better idea? Suggest a change

9.5.6. isZero_factor_zero_of_hom_eq_zero🔗

If all morphisms from the first HN factor A_1 to E are zero, then A_1 = 0. More precisely, the first triangle's third vertex is a zero object.

Proof: By chain_hom_eq_zero_of_factor_zero, all maps from A_1 to the chain object E_1 are zero. Since E_0 = 0, the first triangle gives E_1 \cong A_1, so the identity \mathrm{id}_{A_1} = 0, whence A_1 is zero.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.isZero_factor_zero_of_hom_eq_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) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (hn : 0 < F.n)
  (hzero : ∀ (f : (F.triangle ⟨0, hn⟩).obj₃ ⟶ E), f = 0) :
  CategoryTheory.Limits.IsZero (F.triangle ⟨0, hn⟩).obj₃
CategoryTheory.Triangulated.HNFiltration.isZero_factor_zero_of_hom_eq_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)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < F.n)
  (hzero :
    ∀ (f : (F.triangle ⟨0, hn⟩).obj₃ ⟶ E),
      f = 0) :
  CategoryTheory.Limits.IsZero
    (F.triangle ⟨0, hn⟩).obj₃

Something wrong, better idea? Suggest a change

9.5.7. phiPlus_le_of_nonzero_factor🔗

The highest phase \phi^+(F_1) of one HN filtration cannot exceed \phi^+(F_2) of another, provided F_1 has a nonzero first factor.

Proof: By contradiction: if \phi^+(F_1) > \phi^+(F_2), then all F_2-phases lie below \phi_1(F_1), so \operatorname{Hom}(A_1^{(1)}, E) = 0 by hom_eq_zero_of_gt_phases. Then isZero_factor_zero_of_hom_eq_zero gives A_1^{(1)} = 0, contradicting the hypothesis.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.phiPlus_le_of_nonzero_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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F₁ F₂ : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne : ¬CategoryTheory.Limits.IsZero (F₁.triangle ⟨0, hn₁⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus C F₁ hn₁ ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus C F₂ hn₂
CategoryTheory.Triangulated.HNFiltration.phiPlus_le_of_nonzero_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F₁ F₂ :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne :
    ¬CategoryTheory.Limits.IsZero
        (F₁.triangle ⟨0, hn₁⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus
      C F₁ hn₁ ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus
      C F₂ hn₂

Something wrong, better idea? Suggest a change

9.5.8. phiPlus_eq_of_nonzero_factors🔗

For any two HN filtrations of the same nonzero object, if both have nonzero first factors, then their highest phases agree: \phi^+(F_1) = \phi^+(F_2).

Proof: Antisymmetry from two applications of phiPlus_le_of_nonzero_factor.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.phiPlus_eq_of_nonzero_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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F₁ F₂ : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₁ : ¬CategoryTheory.Limits.IsZero (F₁.triangle ⟨0, hn₁⟩).obj₃)
  (hne₂ : ¬CategoryTheory.Limits.IsZero (F₂.triangle ⟨0, hn₂⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus C F₁ hn₁ =
    CategoryTheory.Triangulated.HNFiltration.phiPlus C F₂ hn₂
CategoryTheory.Triangulated.HNFiltration.phiPlus_eq_of_nonzero_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F₁ F₂ :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₁ :
    ¬CategoryTheory.Limits.IsZero
        (F₁.triangle ⟨0, hn₁⟩).obj₃)
  (hne₂ :
    ¬CategoryTheory.Limits.IsZero
        (F₂.triangle ⟨0, hn₂⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus
      C F₁ hn₁ =
    CategoryTheory.Triangulated.HNFiltration.phiPlus
      C F₂ hn₂

Something wrong, better idea? Suggest a change

9.5.9. isZero_factor_last_of_hom_eq_zero🔗

If all morphisms from E to the last HN factor A_n are zero, then A_n = 0. Dual of isZero_factor_zero_of_hom_eq_zero.

Proof: Since T.\mathrm{mor}_2 = 0 (because it factors through E), the Yoneda exact sequence gives \mathrm{id}_{A_n} = T.\mathrm{mor}_3 \circ \gamma for some \gamma : E_1[1] \to A_n. Hom-vanishing on the shifted prefix filtration shows \gamma = 0, so \mathrm{id}_{A_n} = 0 and A_n is zero.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.isZero_factor_last_of_hom_eq_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) {E : C}
  (G : CategoryTheory.Triangulated.HNFiltration C s.P E) (hn : 0 < G.n)
  (hzero : ∀ (f : E ⟶ (G.triangle ⟨G.n - 1, ⋯⟩).obj₃), f = 0) :
  CategoryTheory.Limits.IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃
CategoryTheory.Triangulated.HNFiltration.isZero_factor_last_of_hom_eq_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)
  {E : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < G.n)
  (hzero :
    ∀
      (f :
        E ⟶
          (G.triangle ⟨G.n - 1, ⋯⟩).obj₃),
      f = 0) :
  CategoryTheory.Limits.IsZero
    (G.triangle ⟨G.n - 1, ⋯⟩).obj₃

Something wrong, better idea? Suggest a change

9.5.10. phiMinus_ge_of_nonzero_last_factor🔗

The lowest phase of one HN filtration is bounded below by the lowest phase of any other, provided the second has a nonzero last factor. Dual of phiPlus_le_of_nonzero_factor.

Proof: By contradiction: if \phi^-(F_1) > \phi^-(F_2), then all F_1-phases exceed the last F_2-phase, so \operatorname{Hom}(E, A_n^{(2)}) = 0 by hom_eq_zero_of_lt_phases, and isZero_factor_last_of_hom_eq_zero gives A_n^{(2)} = 0, a contradiction.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.phiMinus_ge_of_nonzero_last_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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F₁ F₂ : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₂ :
    ¬CategoryTheory.Limits.IsZero (F₂.triangle ⟨F₂.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C F₁ hn₁ ≤
    CategoryTheory.Triangulated.HNFiltration.phiMinus C F₂ hn₂
CategoryTheory.Triangulated.HNFiltration.phiMinus_ge_of_nonzero_last_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F₁ F₂ :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₂ :
    ¬CategoryTheory.Limits.IsZero
        (F₂.triangle
            ⟨F₂.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
      C F₁ hn₁ ≤
    CategoryTheory.Triangulated.HNFiltration.phiMinus
      C F₂ hn₂

Something wrong, better idea? Suggest a change

9.5.11. phiMinus_eq_of_nonzero_last_factors🔗

For any two HN filtrations of the same nonzero object with nonzero last factors, the lowest phases agree: \phi^-(F_1) = \phi^-(F_2).

Proof: Antisymmetry from two applications of phiMinus_ge_of_nonzero_last_factor.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.phiMinus_eq_of_nonzero_last_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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F₁ F₂ : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₁ :
    ¬CategoryTheory.Limits.IsZero (F₁.triangle ⟨F₁.n - 1, ⋯⟩).obj₃)
  (hne₂ :
    ¬CategoryTheory.Limits.IsZero (F₂.triangle ⟨F₂.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C F₁ hn₁ =
    CategoryTheory.Triangulated.HNFiltration.phiMinus C F₂ hn₂
CategoryTheory.Triangulated.HNFiltration.phiMinus_eq_of_nonzero_last_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F₁ F₂ :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn₁ : 0 < F₁.n) (hn₂ : 0 < F₂.n)
  (hne₁ :
    ¬CategoryTheory.Limits.IsZero
        (F₁.triangle ⟨F₁.n - 1, ⋯⟩).obj₃)
  (hne₂ :
    ¬CategoryTheory.Limits.IsZero
        (F₂.triangle
            ⟨F₂.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
      C F₁ hn₁ =
    CategoryTheory.Triangulated.HNFiltration.phiMinus
      C F₂ hn₂

Something wrong, better idea? Suggest a change

9.5.12. exists_both_nonzero🔗

For any nonzero object E, there exists an HN filtration with both a nonzero first factor and a nonzero last factor.

Proof: Start from a filtration with nonzero first factor (from exists_nonzero_first). If the last factor is zero, drop it (preserving the nonzero first factor). Iterate until the last factor is also nonzero; termination is guaranteed by the decreasing filtration length.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.exists_both_nonzero.{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) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero (F.triangle ⟨0, hn⟩).obj₃ ∧
        ¬CategoryTheory.Limits.IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
CategoryTheory.Triangulated.HNFiltration.exists_both_nonzero.{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) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero
            (F.triangle ⟨0, hn⟩).obj₃ ∧
        ¬CategoryTheory.Limits.IsZero
            (F.triangle ⟨F.n - 1, ⋯⟩).obj₃

Something wrong, better idea? Suggest a change

9.5.13. phiPlus_eq🔗

The intrinsic \phi^+(E) equals \phi_1 of any HN filtration of E with nonzero first factor.

Proof: By phiPlus_eq_of_nonzero_factors, applied to the chosen representative filtration and the given one.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_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)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (G : CategoryTheory.Triangulated.HNFiltration C s.P E) (hn : 0 < G.n)
  (hne : ¬CategoryTheory.Limits.IsZero (G.triangle ⟨0, hn⟩).obj₃) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE = G.φ ⟨0, hn⟩
CategoryTheory.Triangulated.Slicing.phiPlus_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)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < G.n)
  (hne :
    ¬CategoryTheory.Limits.IsZero
        (G.triangle ⟨0, hn⟩).obj₃) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE =
    G.φ ⟨0, hn⟩

Something wrong, better idea? Suggest a change

9.5.14. phiMinus_eq🔗

The intrinsic \phi^-(E) equals \phi_n of any HN filtration of E with nonzero last factor.

Proof: By phiMinus_eq_of_nonzero_last_factors, applied to the chosen representative filtration and the given one.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_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)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (G : CategoryTheory.Triangulated.HNFiltration C s.P E) (hn : 0 < G.n)
  (hne : ¬CategoryTheory.Limits.IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.Slicing.phiMinus C s E hE =
    G.φ ⟨G.n - 1, ⋯⟩
CategoryTheory.Triangulated.Slicing.phiMinus_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)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < G.n)
  (hne :
    ¬CategoryTheory.Limits.IsZero
        (G.triangle ⟨G.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE =
    G.φ ⟨G.n - 1, ⋯⟩

Something wrong, better idea? Suggest a change

9.5.15. phiMinus_le_phiPlus🔗

For any nonzero object E, \phi^-(E) \le \phi^+(E).

Proof: By contradiction: if \phi^- > \phi^+, then all phases of one filtration exceed all phases of another, creating a phase gap. Then \operatorname{Hom}(E, E) = 0, so \mathrm{id}_E = 0, contradicting E \ne 0.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_le_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)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.Slicing.phiMinus C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiPlus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_le_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)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE ≤
    CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.16. exists_HN_intrinsic_width🔗

For any nonzero object E, there exists an HN filtration whose extreme phases match the intrinsic \phi^+(E) and \phi^-(E).

Proof: Take a filtration with both nonzero boundary factors (from exists_both_nonzero); then phiPlus_eq and phiMinus_eq identify the extreme phases.

🔗theorem
CategoryTheory.Triangulated.Slicing.exists_HN_intrinsic_width.{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) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      F.φ ⟨0, hn⟩ =
          CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ∧
        F.φ ⟨F.n - 1, ⋯⟩ =
          CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.exists_HN_intrinsic_width.{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) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      F.φ ⟨0, hn⟩ =
          CategoryTheory.Triangulated.Slicing.phiPlus
            C s E hE ∧
        F.φ ⟨F.n - 1, ⋯⟩ =
          CategoryTheory.Triangulated.Slicing.phiMinus
            C s E hE

Something wrong, better idea? Suggest a change

9.5.17. phiPlus_le_phiPlus_of_hn🔗

The intrinsic \phi^+(E) is bounded above by the highest phase of any HN filtration of E.

Proof: By phiPlus_le_of_nonzero_factor applied to a filtration with nonzero first factor.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_le_phiPlus_of_hn.{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)
  (G : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus C G hn
CategoryTheory.Triangulated.Slicing.phiPlus_le_phiPlus_of_hn.{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)
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus
      C G hn

Something wrong, better idea? Suggest a change

9.5.18. phiPlus_lt_of_intervalProp🔗

If E \in \mathcal{P}((a, b)) and E is nonzero, then \phi^+(E) < b.

Proof: The interval property provides a filtration with all phases < b; the intrinsic \phi^+ is bounded by the highest phase of this filtration.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_intervalProp.{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) {a b : ℝ}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < b
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_intervalProp.{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)
  {a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE <
    b

Something wrong, better idea? Suggest a change

9.5.19. phiPlus_gt_of_intervalProp🔗

If E \in \mathcal{P}((a, b)) and E is nonzero, then a < \phi^+(E).

Proof: By contradiction: if \phi^+(E) \le a, then all phases of one filtration are \le a while the interval filtration has all phases > a, creating a phase gap that forces \mathrm{id}_E = 0.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_gt_of_intervalProp.{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) {a b : ℝ}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  a < CategoryTheory.Triangulated.Slicing.phiPlus C s E hE
CategoryTheory.Triangulated.Slicing.phiPlus_gt_of_intervalProp.{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)
  {a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  a <
    CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.20. phiMinus_lt_of_intervalProp🔗

If E \in \mathcal{P}((a, b)) and E is nonzero, then \phi^-(E) < b.

Proof: Follows from \phi^-(E) \le \phi^+(E) < b.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_lt_of_intervalProp.{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) {a b : ℝ}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.phiMinus C s E hE < b
CategoryTheory.Triangulated.Slicing.phiMinus_lt_of_intervalProp.{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)
  {a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE <
    b

Something wrong, better idea? Suggest a change

9.5.21. phiMinus_gt_of_intervalProp🔗

If E \in \mathcal{P}((a, b)) and E is nonzero, then a < \phi^-(E).

Proof: The interval filtration has lowest phase > a; the intrinsic \phi^- is bounded below by this filtration's lowest phase.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_intervalProp.{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) {a b : ℝ}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  a < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_intervalProp.{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)
  {a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  a <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.22. phiMinus_ge_phiMinus_of_hn🔗

The intrinsic \phi^-(E) is bounded below by the lowest phase of any HN filtration of E. Dual of phiPlus_le_phiPlus_of_hn.

Proof: By phiMinus_ge_of_nonzero_last_factor applied to a filtration with nonzero last factor.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_ge_phiMinus_of_hn.{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)
  (G : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C G hn ≤
    CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_ge_phiMinus_of_hn.{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)
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hn : 0 < G.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
      C G hn ≤
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.23. phiMinus_gt_of_gtProp🔗

If E \in \mathcal{P}(> t) and E is nonzero, then t < \phi^-(E).

Proof: The \mathcal{P}(> t) condition gives a filtration with \phi^- > t; the intrinsic \phi^- is bounded below by this.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_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) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hgt : CategoryTheory.Triangulated.Slicing.gtProp C s t E) :
  t < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_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)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hgt :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t E) :
  t <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.24. phiPlus_le_of_leProp🔗

If E \in \mathcal{P}(\le t) and E is nonzero, then \phi^+(E) \le t.

Proof: The \mathcal{P}(\le t) condition gives a filtration with \phi^+ \le t; the intrinsic \phi^+ is bounded above by this.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_le_of_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) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hle : CategoryTheory.Triangulated.Slicing.leProp C s t E) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ t
CategoryTheory.Triangulated.Slicing.phiPlus_le_of_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)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hle :
    CategoryTheory.Triangulated.Slicing.leProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE ≤
    t

Something wrong, better idea? Suggest a change

9.5.25. phiPlus_lt_of_ltProp🔗

If E \in \mathcal{P}(< t) and E is nonzero, then \phi^+(E) < t.

Proof: The \mathcal{P}(< t) condition gives a filtration with \phi^+ < t.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_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) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hlt : CategoryTheory.Triangulated.Slicing.ltProp C s t E) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < t
CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_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)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hlt :
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t E) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s E hE <
    t

Something wrong, better idea? Suggest a change

9.5.26. phiMinus_ge_of_geProp🔗

If E \in \mathcal{P}(\ge t) and E is nonzero, then t \le \phi^-(E).

Proof: The \mathcal{P}(\ge t) condition gives a filtration with \phi^- \ge t.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_ge_of_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) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hge : CategoryTheory.Triangulated.Slicing.geProp C s t E) :
  t ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s E hE
CategoryTheory.Triangulated.Slicing.phiMinus_ge_of_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)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hge :
    CategoryTheory.Triangulated.Slicing.geProp
      C s t E) :
  t ≤
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s E hE

Something wrong, better idea? Suggest a change

9.5.27. gtProp_of_phiMinus_gt🔗

If t < \phi^-(E), then E \in \mathcal{P}(> t).

Proof: Take a filtration from exists_both_nonzero; its lowest phase equals the intrinsic \phi^-(E) > t.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_of_phiMinus_gt.{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) {t : ℝ}
  (hgt : t < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t E
CategoryTheory.Triangulated.Slicing.gtProp_of_phiMinus_gt.{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)
  {t : ℝ}
  (hgt :
    t <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s t E

Something wrong, better idea? Suggest a change

9.5.28. leProp_of_phiPlus_le🔗

If \phi^+(E) \le t, then E \in \mathcal{P}(\le t).

Proof: Take a filtration from exists_both_nonzero; its highest phase equals the intrinsic \phi^+(E) \le t.

🔗theorem
CategoryTheory.Triangulated.Slicing.leProp_of_phiPlus_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]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {t : ℝ}
  (hle : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ≤ t) :
  CategoryTheory.Triangulated.Slicing.leProp C s t E
CategoryTheory.Triangulated.Slicing.leProp_of_phiPlus_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {t : ℝ}
  (hle :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ≤
      t) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s t E

Something wrong, better idea? Suggest a change

9.5.29. ltProp_of_phiPlus_lt🔗

If \phi^+(E) < t, then E \in \mathcal{P}(< t).

Proof: Take a filtration from exists_both_nonzero; its highest phase equals \phi^+(E) < t.

🔗theorem
CategoryTheory.Triangulated.Slicing.ltProp_of_phiPlus_lt.{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) {t : ℝ}
  (hlt : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < t) :
  CategoryTheory.Triangulated.Slicing.ltProp C s t E
CategoryTheory.Triangulated.Slicing.ltProp_of_phiPlus_lt.{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)
  {t : ℝ}
  (hlt :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE <
      t) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s t E

Something wrong, better idea? Suggest a change

9.5.30. geProp_of_phiMinus_ge🔗

If t \le \phi^-(E), then E \in \mathcal{P}(\ge t).

Proof: Take a filtration from exists_both_nonzero; its lowest phase equals \phi^-(E) \ge t.

🔗theorem
CategoryTheory.Triangulated.Slicing.geProp_of_phiMinus_ge.{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) {t : ℝ}
  (hge : t ≤ CategoryTheory.Triangulated.Slicing.phiMinus C s E hE) :
  CategoryTheory.Triangulated.Slicing.geProp C s t E
CategoryTheory.Triangulated.Slicing.geProp_of_phiMinus_ge.{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)
  {t : ℝ}
  (hge :
    t ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE) :
  CategoryTheory.Triangulated.Slicing.geProp
    C s t E

Something wrong, better idea? Suggest a change

9.5.31. intervalProp_of_intrinsic_phases🔗

If a < \phi^-(E) and \phi^+(E) < b, then E \in \mathcal{P}((a, b)). Converse of the interval-to-phase-bound lemmas.

Proof: Take a filtration from exists_both_nonzero whose extreme phases match the intrinsic values. Then every phase \phi_i satisfies a < \phi^- \le \phi_i \le \phi^+ < b.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_of_intrinsic_phases.{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) {a b : ℝ}
  (hminus : a < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE)
  (hplus : CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < b) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
CategoryTheory.Triangulated.Slicing.intervalProp_of_intrinsic_phases.{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)
  {a b : ℝ}
  (hminus :
    a <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C s E hE)
  (hplus :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE <
      b) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b E

Something wrong, better idea? Suggest a change

9.5.32. phase_le_phiPlus_of_nonzero_hom🔗

If a semistable object A \in \mathcal{P}(\phi) maps nonzero to X, then \phi \le \phi^+(X). Contrapositive of hom_eq_zero_of_gt_phases.

Proof: By contradiction: if \phi > \phi^+(X), then all phases of any filtration of X lie below \phi, so hom_eq_zero_of_gt_phases kills the morphism.

🔗theorem
CategoryTheory.Triangulated.Slicing.phase_le_phiPlus_of_nonzero_hom.{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 X : C} {φ : ℝ}
  (hA : s.P φ A) (hX : ¬CategoryTheory.Limits.IsZero X) (f : A ⟶ X)
  (hf : f ≠ 0) :
  φ ≤ CategoryTheory.Triangulated.Slicing.phiPlus C s X hX
CategoryTheory.Triangulated.Slicing.phase_le_phiPlus_of_nonzero_hom.{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 X : C} {φ : ℝ} (hA : s.P φ A)
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (f : A ⟶ X) (hf : f ≠ 0) :
  φ ≤
    CategoryTheory.Triangulated.Slicing.phiPlus
      C s X hX

Something wrong, better idea? Suggest a change

9.5.33. phiMinus_le_phase_of_nonzero_hom🔗

If X maps nonzero to a semistable object B \in \mathcal{P}(\psi), then \phi^-(X) \le \psi. Contrapositive of hom_eq_zero_of_lt_phases.

Proof: By contradiction: if \phi^-(X) > \psi, then all phases of X exceed \psi, so hom_eq_zero_of_lt_phases kills the morphism.

🔗theorem
CategoryTheory.Triangulated.Slicing.phiMinus_le_phase_of_nonzero_hom.{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 B : C} {ψ : ℝ}
  (hB : s.P ψ B) (hX : ¬CategoryTheory.Limits.IsZero X) (f : X ⟶ B)
  (hf : f ≠ 0) :
  CategoryTheory.Triangulated.Slicing.phiMinus C s X hX ≤ ψ
CategoryTheory.Triangulated.Slicing.phiMinus_le_phase_of_nonzero_hom.{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 B : C} {ψ : ℝ} (hB : s.P ψ B)
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (f : X ⟶ B) (hf : f ≠ 0) :
  CategoryTheory.Triangulated.Slicing.phiMinus
      C s X hX ≤
    ψ

Something wrong, better idea? Suggest a change