9.4. Slicing: HNOperations🔗

9.4.1. prefix_phiMinus_gt🔗

The prefix of an HN filtration truncated at step k has lowest phase \phi^-(\text{prefix}) > t provided every phase \phi_j for j < k exceeds t.

Proof: The lowest phase of the prefix is \phi_{k-1}, which is among the phases bounded below by t by hypothesis.

theorem

CategoryTheory.Triangulated.HNFiltration.prefix_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]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (t : ℝ)
  (ht : ∀ (j : Fin k), t < F.φ ⟨↑j, ⋯⟩) :
  t <
    CategoryTheory.Triangulated.HNFiltration.phiMinus C
      (CategoryTheory.Triangulated.HNFiltration.prefix C F k hk hk0) hk0
CategoryTheory.Triangulated.HNFiltration.prefix_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]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (t : ℝ)
  (ht : ∀ (j : Fin k), t < F.φ ⟨↑j, ⋯⟩) :
  t <
    CategoryTheory.Triangulated.HNFiltration.phiMinus
      C
      (CategoryTheory.Triangulated.HNFiltration.prefix
        C F k hk hk0)
      hk0

Something wrong, better idea? Suggest a change

9.4.2. chain_obj_gtProp🔗

The chain object E_k at the split point of an HN filtration satisfies \mathcal{P}(> t) if all phases before the split are > t.

Proof: The prefix filtration provides an HN filtration of E_k whose phases are all > t, giving the result via the definition of \mathcal{P}(> t).

theorem

CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (t : ℝ)
  (ht : ∀ (j : Fin k), t < F.φ ⟨↑j, ⋯⟩) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t (F.chain.obj ⟨k, ⋯⟩)
CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (t : ℝ)
  (ht : ∀ (j : Fin k), t < F.φ ⟨↑j, ⋯⟩) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s t (F.chain.obj ⟨k, ⋯⟩)

Something wrong, better idea? Suggest a change

9.4.3. chain_obj_leProp🔗

The chain object E_k at the split point of an HN filtration satisfies \mathcal{P}(\le t) if all phases before the split are \le t.

Proof: The prefix filtration of E_k has highest phase \phi_1 among the first k phases, all of which are \le t.

theorem

CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (t : ℝ)
  (ht : ∀ (j : Fin k), F.φ ⟨↑j, ⋯⟩ ≤ t) :
  CategoryTheory.Triangulated.Slicing.leProp C s t (F.chain.obj ⟨k, ⋯⟩)
CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (t : ℝ)
  (ht : ∀ (j : Fin k), F.φ ⟨↑j, ⋯⟩ ≤ t) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s t (F.chain.obj ⟨k, ⋯⟩)

Something wrong, better idea? Suggest a change

9.4.4. chain_obj_ltProp🔗

The chain object E_k at the split point of an HN filtration satisfies \mathcal{P}(< t) if all phases before the split are < t.

Proof: Analogous to chain_obj_leProp with strict inequality: the prefix's highest phase \phi_1 < t.

theorem

CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (t : ℝ)
  (ht : ∀ (j : Fin k), F.φ ⟨↑j, ⋯⟩ < t) :
  CategoryTheory.Triangulated.Slicing.ltProp C s t (F.chain.obj ⟨k, ⋯⟩)
CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (t : ℝ)
  (ht : ∀ (j : Fin k), F.φ ⟨↑j, ⋯⟩ < t) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s t (F.chain.obj ⟨k, ⋯⟩)

Something wrong, better idea? Suggest a change

9.4.5. chain_obj_geProp🔗

The chain object E_k at the split point of an HN filtration satisfies \mathcal{P}(\ge t) if all phases before the split are \ge t.

Proof: The prefix filtration's lowest phase \phi_{k-1} \ge t by hypothesis.

theorem

CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (t : ℝ)
  (ht : ∀ (j : Fin k), t ≤ F.φ ⟨↑j, ⋯⟩) :
  CategoryTheory.Triangulated.Slicing.geProp C s t (F.chain.obj ⟨k, ⋯⟩)
CategoryTheory.Triangulated.HNFiltration.chain_obj_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (t : ℝ)
  (ht : ∀ (j : Fin k), t ≤ F.φ ⟨↑j, ⋯⟩) :
  CategoryTheory.Triangulated.Slicing.geProp
    C s t (F.chain.obj ⟨k, ⋯⟩)

Something wrong, better idea? Suggest a change

9.4.6. gtProp_of_hn🔗

An HN-filtered object E satisfies \mathcal{P}(> t) if all its phases are > t and the filtration length is positive.

Proof: Direct from the definition: the lowest phase \phi^- = \phi_{n} is > t by hypothesis.

theorem

CategoryTheory.Triangulated.Slicing.gtProp_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (t : ℝ)
  (ht : ∀ (j : Fin F.n), t < F.φ j) (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.gtProp C s t E
CategoryTheory.Triangulated.Slicing.gtProp_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (t : ℝ)
  (ht : ∀ (j : Fin F.n), t < F.φ j)
  (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s t E

Something wrong, better idea? Suggest a change

9.4.7. leProp_of_hn🔗

An HN-filtered object E satisfies \mathcal{P}(\le t) if all its phases are \le t and the filtration length is positive.

Proof: Direct from the definition: the highest phase \phi^+ = \phi_1 \le t by hypothesis.

theorem

CategoryTheory.Triangulated.Slicing.leProp_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (t : ℝ)
  (ht : ∀ (j : Fin F.n), F.φ j ≤ t) (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.leProp C s t E
CategoryTheory.Triangulated.Slicing.leProp_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (t : ℝ)
  (ht : ∀ (j : Fin F.n), F.φ j ≤ t)
  (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.leProp
    C s t E

Something wrong, better idea? Suggest a change

9.4.8. geProp_of_hn🔗

An HN-filtered object E satisfies \mathcal{P}(\ge t) if all its phases are \ge t and the filtration length is positive.

Proof: Direct from the definition: the lowest phase \phi^- = \phi_n \ge t by hypothesis.

theorem

CategoryTheory.Triangulated.Slicing.geProp_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (t : ℝ)
  (ht : ∀ (j : Fin F.n), t ≤ F.φ j) (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.geProp C s t E
CategoryTheory.Triangulated.Slicing.geProp_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (t : ℝ)
  (ht : ∀ (j : Fin F.n), t ≤ F.φ j)
  (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.geProp
    C s t E

Something wrong, better idea? Suggest a change

9.4.9. ltProp_of_hn🔗

An HN-filtered object E satisfies \mathcal{P}(< t) if all its phases are < t and the filtration length is positive.

Proof: Direct from the definition: the highest phase \phi^+ = \phi_1 < t by hypothesis.

theorem

CategoryTheory.Triangulated.Slicing.ltProp_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}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (t : ℝ)
  (ht : ∀ (j : Fin F.n), F.φ j < t) (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.ltProp C s t E
CategoryTheory.Triangulated.Slicing.ltProp_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}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (t : ℝ)
  (ht : ∀ (j : Fin F.n), F.φ j < t)
  (hn : 0 < F.n) :
  CategoryTheory.Triangulated.Slicing.ltProp
    C s t E

Something wrong, better idea? Suggest a change

9.4.10. appendFactor🔗

Extend an HN filtration by appending one semistable factor via a distinguished triangle. Given an HN filtration G of Y' and a distinguished triangle Y' \to Z \to F \to Y'[1] where F \in \mathcal{P}(\psi) with \psi strictly less than all phases of G, produce an HN filtration of Z with the additional factor F appended at the end.

Construction: Constructs a new composable-arrows chain of length n + 1 by extending the existing chain with the new object Z as the top. The phase assignment appends \psi after the existing phases. Strict antitonicity of the extended phase sequence follows from \psi < \phi_j for all existing phases.

def

CategoryTheory.Triangulated.HNFiltration.appendFactor.{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} {Y' Z : C}
  (G : CategoryTheory.Triangulated.HNFiltration C P Y')
  (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (eT₁ : T.obj₁ ≅ Y') (eT₂ : T.obj₂ ≅ Z) (ψ : ℝ) (hψ : P ψ T.obj₃)
  (hψ_lt : ∀ (j : Fin G.n), ψ < G.φ j) :
  CategoryTheory.Triangulated.HNFiltration C P Z
CategoryTheory.Triangulated.HNFiltration.appendFactor.{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}
  {Y' Z : C}
  (G :
    CategoryTheory.Triangulated.HNFiltration
      C P Y')
  (T :
    CategoryTheory.Pretriangulated.Triangle
      C)
  (hT :
    T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (eT₁ : T.obj₁ ≅ Y') (eT₂ : T.obj₂ ≅ Z)
  (ψ : ℝ) (hψ : P ψ T.obj₃)
  (hψ_lt : ∀ (j : Fin G.n), ψ < G.φ j) :
  CategoryTheory.Triangulated.HNFiltration
    C P Z

Something wrong, better idea? Suggest a change

9.4.11. gtProp_closedUnderIso🔗

The property \mathcal{P}(> t) is closed under isomorphisms: if E \cong E' and E \in \mathcal{P}(> t), then E' \in \mathcal{P}(> t).

Proof: Zero objects are preserved under isomorphisms. For the non-zero case, transport the HN filtration across the isomorphism using HNFiltration.ofIso.

theorem

CategoryTheory.Triangulated.Slicing.gtProp_closedUnderIso.{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).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.Slicing.gtProp_closedUnderIso.{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).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

9.4.12. leProp_closedUnderIso🔗

The property \mathcal{P}(\le t) is closed under isomorphisms.

Proof: Transport the HN filtration across the isomorphism using HNFiltration.ofIso; the phase bounds are preserved.

theorem

CategoryTheory.Triangulated.Slicing.leProp_closedUnderIso.{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).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.Slicing.leProp_closedUnderIso.{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).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

9.4.13. ltProp_closedUnderIso🔗

The property \mathcal{P}(< t) is closed under isomorphisms.

Proof: Transport the HN filtration across the isomorphism using HNFiltration.ofIso; the strict phase bounds are preserved.

theorem

CategoryTheory.Triangulated.Slicing.ltProp_closedUnderIso.{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).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.Slicing.ltProp_closedUnderIso.{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).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

9.4.14. geProp_closedUnderIso🔗

The property \mathcal{P}(\ge t) is closed under isomorphisms.

Proof: Transport the HN filtration across the isomorphism using HNFiltration.ofIso; the phase bounds are preserved.

theorem

CategoryTheory.Triangulated.Slicing.geProp_closedUnderIso.{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).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.Slicing.geProp_closedUnderIso.{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).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change