9.1. Slicing: Basic🔗

9.1.1. phiMinus_le_phiPlus🔗

For any HN filtration 0 = E_0 \to E_1 \to \cdots \to E_n = E with n > 0, the lowest phase \phi^-(F) = \phi_n satisfies \phi^-(F) \le \phi^+(F) = \phi_1. In other words, the highest phase is at least the lowest phase.

Proof: Immediate from strict antitonicity of the phase sequence: \phi_1 > \phi_2 > \cdots > \phi_n.

theorem

CategoryTheory.Triangulated.HNFiltration.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]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C F h ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus C F h
CategoryTheory.Triangulated.HNFiltration.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]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
      C F h ≤
    CategoryTheory.Triangulated.HNFiltration.phiPlus
      C F h

Something wrong, better idea? Suggest a change

9.1.2. phase_mem_range🔗

Every phase \phi_i of an HN filtration lies in the interval [\phi^-(F),\, \phi^+(F)]. That is, \phi^- \le \phi_i \le \phi^+ for all i.

Proof: Both inequalities follow directly from the strict antitonicity of the phase assignment via the monotonicity of the index comparison.

theorem

CategoryTheory.Triangulated.HNFiltration.phase_mem_range.{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}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (h : 0 < F.n)
  (i : Fin F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C F h ≤ F.φ i ∧
    F.φ i ≤ CategoryTheory.Triangulated.HNFiltration.phiPlus C F h
CategoryTheory.Triangulated.HNFiltration.phase_mem_range.{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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (h : 0 < F.n) (i : Fin F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
        C F h ≤
      F.φ i ∧
    F.φ i ≤
      CategoryTheory.Triangulated.HNFiltration.phiPlus
        C F h

Something wrong, better idea? Suggest a change

9.1.3. leProp🔗

The subcategory predicate \mathcal{P}(\le t): an object E satisfies this if it is zero or admits an HN filtration whose highest phase \phi^+(F) \le t.

Construction: Defined as the disjunction: E is zero, or there exists an HN filtration F of E with 0 < n and \phi^+(F) \le t.

def

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

9.1.4. gtProp🔗

The subcategory predicate \mathcal{P}(> t): an object E satisfies this if it is zero or admits an HN filtration whose lowest phase \phi^-(F) > t.

Construction: Defined as the disjunction: E is zero, or there exists an HN filtration F of E with 0 < n and t < \phi^-(F).

def

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

9.1.5. ltProp🔗

The subcategory predicate \mathcal{P}(< t): an object E satisfies this if it is zero or admits an HN filtration whose highest phase \phi^+(F) < t.

Construction: Defined as the disjunction: E is zero, or there exists an HN filtration F of E with 0 < n and \phi^+(F) < t.

def

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

9.1.6. geProp🔗

The subcategory predicate \mathcal{P}(\ge t): an object E satisfies this if it is zero or admits an HN filtration whose lowest phase \phi^-(F) \ge t.

Construction: Defined as the disjunction: E is zero, or there exists an HN filtration F of E with 0 < n and t \le \phi^-(F).

def

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

9.1.7. leProp_zero🔗

The zero object lies in \mathcal{P}(\le t) for every t \in \mathbb{R}.

Proof: By the left disjunct of the definition: the zero object is zero.

theorem

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.leProp C s t 0
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s t 0

Something wrong, better idea? Suggest a change

9.1.8. gtProp_zero🔗

The zero object lies in \mathcal{P}(> t) for every t \in \mathbb{R}.

Proof: By the left disjunct of the definition: the zero object is zero.

theorem

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t 0
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s t 0

Something wrong, better idea? Suggest a change

9.1.9. leProp_mono🔗

The subcategory predicates are monotone in the parameter: if t_1 \le t_2 then \mathcal{P}(\le t_1) \subseteq \mathcal{P}(\le t_2).

Proof: If \phi^+(F) \le t_1 \le t_2, then \phi^+(F) \le t_2 by transitivity.

theorem

CategoryTheory.Triangulated.Slicing.leProp_mono.{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₁ t₂ : ℝ}
  (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.leProp C s t₁ ≤
    CategoryTheory.Triangulated.Slicing.leProp C s t₂
CategoryTheory.Triangulated.Slicing.leProp_mono.{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₁ t₂ : ℝ} (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.leProp
      C s t₁ ≤
    CategoryTheory.Triangulated.Slicing.leProp
      C s t₂

Something wrong, better idea? Suggest a change

9.1.10. gtProp_anti🔗

The subcategory predicate \mathcal{P}(> \cdot) is antitone: if t_1 \le t_2 then \mathcal{P}(> t_2) \subseteq \mathcal{P}(> t_1).

Proof: If t_2 < \phi^-(F) and t_1 \le t_2, then t_1 < \phi^-(F).

theorem

CategoryTheory.Triangulated.Slicing.gtProp_anti.{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₁ t₂ : ℝ}
  (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t₂ ≤
    CategoryTheory.Triangulated.Slicing.gtProp C s t₁
CategoryTheory.Triangulated.Slicing.gtProp_anti.{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₁ t₂ : ℝ} (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.gtProp
      C s t₂ ≤
    CategoryTheory.Triangulated.Slicing.gtProp
      C s t₁

Something wrong, better idea? Suggest a change

9.1.11. ltProp_zero🔗

The zero object lies in \mathcal{P}(< t) for every t \in \mathbb{R}.

Proof: By the left disjunct of the definition: the zero object is zero.

theorem

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.ltProp C s t 0
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s t 0

Something wrong, better idea? Suggest a change

9.1.12. geProp_zero🔗

The zero object lies in \mathcal{P}(\ge t) for every t \in \mathbb{R}.

Proof: By the left disjunct of the definition: the zero object is zero.

theorem

CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.geProp C s t 0
CategoryTheory.Triangulated.Slicing.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 : ℝ) :
  CategoryTheory.Triangulated.Slicing.geProp
    C s t 0

Something wrong, better idea? Suggest a change

9.1.13. ltProp_mono🔗

The subcategory predicate \mathcal{P}(< \cdot) is monotone: if t_1 \le t_2 then \mathcal{P}(< t_1) \subseteq \mathcal{P}(< t_2).

Proof: If \phi^+(F) < t_1 \le t_2, then \phi^+(F) < t_2.

theorem

CategoryTheory.Triangulated.Slicing.ltProp_mono.{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₁ t₂ : ℝ}
  (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.ltProp C s t₁ ≤
    CategoryTheory.Triangulated.Slicing.ltProp C s t₂
CategoryTheory.Triangulated.Slicing.ltProp_mono.{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₁ t₂ : ℝ} (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.ltProp
      C s t₁ ≤
    CategoryTheory.Triangulated.Slicing.ltProp
      C s t₂

Something wrong, better idea? Suggest a change

9.1.14. geProp_anti🔗

The subcategory predicate \mathcal{P}(\ge \cdot) is antitone: if t_1 \le t_2 then \mathcal{P}(\ge t_2) \subseteq \mathcal{P}(\ge t_1).

Proof: If t_2 \le \phi^-(F) and t_1 \le t_2, then t_1 \le \phi^-(F).

theorem

CategoryTheory.Triangulated.Slicing.geProp_anti.{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₁ t₂ : ℝ}
  (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.geProp C s t₂ ≤
    CategoryTheory.Triangulated.Slicing.geProp C s t₁
CategoryTheory.Triangulated.Slicing.geProp_anti.{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₁ t₂ : ℝ} (h : t₁ ≤ t₂) :
  CategoryTheory.Triangulated.Slicing.geProp
      C s t₂ ≤
    CategoryTheory.Triangulated.Slicing.geProp
      C s t₁

Something wrong, better idea? Suggest a change

9.1.15. leProp_of_ltProp🔗

\mathcal{P}(< t) \subseteq \mathcal{P}(\le t): a strict upper phase bound implies a non-strict one.

Proof: Immediate from \phi^+(F) < t \implies \phi^+(F) \le t.

theorem

CategoryTheory.Triangulated.Slicing.leProp_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) {t : ℝ} :
  CategoryTheory.Triangulated.Slicing.ltProp C s t ≤
    CategoryTheory.Triangulated.Slicing.leProp C s t
CategoryTheory.Triangulated.Slicing.leProp_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)
  {t : ℝ} :
  CategoryTheory.Triangulated.Slicing.ltProp
      C s t ≤
    CategoryTheory.Triangulated.Slicing.leProp
      C s t

Something wrong, better idea? Suggest a change

9.1.16. geProp_of_gtProp🔗

\mathcal{P}(> t) \subseteq \mathcal{P}(\ge t): a strict lower phase bound implies a non-strict one.

Proof: Immediate from t < \phi^-(F) \implies t \le \phi^-(F).

theorem

CategoryTheory.Triangulated.Slicing.geProp_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) {t : ℝ} :
  CategoryTheory.Triangulated.Slicing.gtProp C s t ≤
    CategoryTheory.Triangulated.Slicing.geProp C s t
CategoryTheory.Triangulated.Slicing.geProp_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)
  {t : ℝ} :
  CategoryTheory.Triangulated.Slicing.gtProp
      C s t ≤
    CategoryTheory.Triangulated.Slicing.geProp
      C s t

Something wrong, better idea? Suggest a change

9.1.17. ltProp_of_intervalProp🔗

If E \in \mathcal{P}((a, b)) (all HN phases in the open interval), then E \in \mathcal{P}(< b).

Proof: The interval condition gives \phi_i < b for all factors; the first factor's phase is \phi^+(F) < b.

theorem

CategoryTheory.Triangulated.Slicing.ltProp_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) {a b : ℝ} {E : C}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.ltProp C s b E
CategoryTheory.Triangulated.Slicing.ltProp_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)
  {a b : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s b E

Something wrong, better idea? Suggest a change

9.1.18. chain_hom_eq_zero_of_gt🔗

Any morphism from a semistable object A \in \mathcal{P}(\psi) to the k-th chain object E_k of an HN filtration whose phases all satisfy \phi_i < \psi is zero.

Proof: Induction on k. The base k = 0 is trivial since E_0 = 0. For the inductive step, the coYoneda exact sequence on the k-th distinguished triangle gives that any map A \to E_k factors through the k-th semistable factor, but \operatorname{Hom}(A, A_k) = 0 by the phase gap axiom.

theorem

CategoryTheory.Triangulated.chain_hom_eq_zero_of_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) {A E : C} {ψ : ℝ}
  (hA : s.P ψ A) (F : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ) (k : ℕ) (hk : k < F.n + 1)
  (f : A ⟶ F.chain.obj ⟨k, hk⟩) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_of_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)
  {A E : C} {ψ : ℝ} (hA : s.P ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ)
  (k : ℕ) (hk : k < F.n + 1)
  (f : A ⟶ F.chain.obj ⟨k, hk⟩) : f = 0

Something wrong, better idea? Suggest a change

9.1.19. hom_eq_zero_of_gt_phases🔗

A morphism from a semistable object A \in \mathcal{P}(\psi) to an HN-filtered object E whose phases are all strictly less than \psi is zero.

Proof: Follows from chain_hom_eq_zero_of_gt applied at the top of the chain, using the isomorphism E_n \cong E.

theorem

CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_gt_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) {A E : C} {ψ : ℝ}
  (hA : s.P ψ A) (F : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ) (f : A ⟶ E) : f = 0
CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_gt_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)
  {A E : C} {ψ : ℝ} (hA : s.P ψ A)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hlt : ∀ (i : Fin F.n), F.φ i < ψ)
  (f : A ⟶ E) : f = 0

Something wrong, better idea? Suggest a change

9.1.20. chain_hom_eq_zero_gap🔗

Any morphism from the k-th chain object of an HN filtration F_X to an object Y admitting a filtration F_Y is zero, provided every phase of F_X is strictly greater than every phase of F_Y.

Proof: Induction on k. The base is trivial (E_0 = 0). For the inductive step, the Yoneda exact sequence factors the map through the k-th semistable factor of F_X, and hom_eq_zero_of_gt_phases shows this factor maps to zero into Y.

theorem

CategoryTheory.Triangulated.chain_hom_eq_zero_gap.{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}
  (Fx : CategoryTheory.Triangulated.HNFiltration C s.P X)
  (Fy : CategoryTheory.Triangulated.HNFiltration C s.P Y)
  (hgap : ∀ (i : Fin Fx.n) (j : Fin Fy.n), Fy.φ j < Fx.φ i) (k : ℕ)
  (hk : k < Fx.n + 1) (f : Fx.chain.obj ⟨k, hk⟩ ⟶ Y) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_gap.{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}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration
      C s.P X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration
      C s.P Y)
  (hgap :
    ∀ (i : Fin Fx.n) (j : Fin Fy.n),
      Fy.φ j < Fx.φ i)
  (k : ℕ) (hk : k < Fx.n + 1)
  (f : Fx.chain.obj ⟨k, hk⟩ ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.1.21. hom_eq_zero_of_phase_gap🔗

If two HN-filtered objects X and Y have a phase gap---every phase of F_X is strictly greater than every phase of F_Y---then \operatorname{Hom}(X, Y) = 0.

Proof: Follows from chain_hom_eq_zero_gap applied at the top of the chain for F_X, using the isomorphism X_n \cong X.

theorem

CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_phase_gap.{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}
  (Fx : CategoryTheory.Triangulated.HNFiltration C s.P X)
  (Fy : CategoryTheory.Triangulated.HNFiltration C s.P Y)
  (hgap : ∀ (i : Fin Fx.n) (j : Fin Fy.n), Fy.φ j < Fx.φ i)
  (f : X ⟶ Y) : f = 0
CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_phase_gap.{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}
  (Fx :
    CategoryTheory.Triangulated.HNFiltration
      C s.P X)
  (Fy :
    CategoryTheory.Triangulated.HNFiltration
      C s.P Y)
  (hgap :
    ∀ (i : Fin Fx.n) (j : Fin Fy.n),
      Fy.φ j < Fx.φ i)
  (f : X ⟶ Y) : f = 0

Something wrong, better idea? Suggest a change

9.1.22. chain_hom_eq_zero_of_lt🔗

Any morphism from the k-th chain object of an HN filtration (whose phases are all strictly greater than \psi) to a semistable object B \in \mathcal{P}(\psi) is zero.

Proof: Induction on k. The base is trivial. For the inductive step, the Yoneda exact sequence factors the map through the k-th semistable factor A_k, and the pointwise Hom-vanishing axiom gives \operatorname{Hom}(A_k, B) = 0 since \phi_k > \psi.

theorem

CategoryTheory.Triangulated.chain_hom_eq_zero_of_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) {B E : C} {ψ : ℝ}
  (hB : s.P ψ B) (F : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hgt : ∀ (i : Fin F.n), ψ < F.φ i) (k : ℕ) (hk : k < F.n + 1)
  (f : F.chain.obj ⟨k, hk⟩ ⟶ B) : f = 0
CategoryTheory.Triangulated.chain_hom_eq_zero_of_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)
  {B E : C} {ψ : ℝ} (hB : s.P ψ B)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hgt : ∀ (i : Fin F.n), ψ < F.φ i)
  (k : ℕ) (hk : k < F.n + 1)
  (f : F.chain.obj ⟨k, hk⟩ ⟶ B) : f = 0

Something wrong, better idea? Suggest a change

9.1.23. hom_eq_zero_of_lt_phases🔗

A morphism from an HN-filtered object E whose phases are all strictly greater than \psi to a semistable object B \in \mathcal{P}(\psi) is zero.

Proof: Follows from chain_hom_eq_zero_of_lt at the top of the chain, using E_n \cong E.

theorem

CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_lt_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) {B E : C} {ψ : ℝ}
  (hB : s.P ψ B) (F : CategoryTheory.Triangulated.HNFiltration C s.P E)
  (hgt : ∀ (i : Fin F.n), ψ < F.φ i) (f : E ⟶ B) : f = 0
CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_lt_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)
  {B E : C} {ψ : ℝ} (hB : s.P ψ B)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (hgt : ∀ (i : Fin F.n), ψ < F.φ i)
  (f : E ⟶ B) : f = 0

Something wrong, better idea? Suggest a change