Boundary factors of owner HN filtrations

This module removes zero factors at either end of a repository-owned Harder--Narasimhan filtration. Consequently every nonzero object admits an HN filtration whose highest and lowest factors are nonzero.

theorem CategoryTheory.Triangulated.HNFiltration.n_pos (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hE : ¬Limits.IsZero E) : 0 < F.n

An HN filtration of a nonzero object contains at least one factor.

theorem CategoryTheory.Triangulated.HNFiltration.exists_nonzero_factor (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hE : ¬Limits.IsZero E) : ∃ (i : Fin F.n), ¬Limits.IsZero (F.factor i)

Some factor of an HN filtration of a nonzero object is nonzero.

noncomputable def CategoryTheory.Triangulated.HNFiltration.dropFirst (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hn : 1 < F.n) (hzero : Limits.IsZero (F.factor ⟨0, ⋯⟩)) : HNFiltration C P E

Remove a zero first factor from an HN filtration.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.Slicing.exists_hn_nonzero_first (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) : ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n), ¬Limits.IsZero (F.factor ⟨0, hn⟩)

A nonzero object admits an HN filtration with nonzero highest factor.

noncomputable def CategoryTheory.Triangulated.HNFiltration.dropLast (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hn : 1 < F.n) (hzero : Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)) : HNFiltration C P E

Remove a zero last factor from an HN filtration.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.Slicing.exists_hn_nonzero_last (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) : ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n), ¬Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)

A nonzero object admits an HN filtration with nonzero lowest factor.

theorem CategoryTheory.Triangulated.Slicing.exists_hn_nonzero_boundaries (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) : ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n), ¬Limits.IsZero (F.factor ⟨0, hn⟩) ∧ ¬Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)

A nonzero object admits one HN filtration with both boundary factors nonzero.