Intrinsic phases of owner slicings

The extremal phases of a nonzero object are independent of the HN filtration used to compute them. This module establishes that uniqueness and defines the repository-owned intrinsic highest and lowest phases.

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

If every map from the first factor to the filtered object vanishes, then every map from that factor to every stage of the filtration vanishes.

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

A first factor is zero when all of its maps to the filtered object vanish.

theorem CategoryTheory.Triangulated.HNFiltration.phiPlus_le_of_firstFactor_nonzero (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} (F G : HNFiltration C s.P E) (hF : 0 < F.n) (hG : 0 < G.n) (hne : ¬Limits.IsZero (F.factor ⟨0, hF⟩)) : phiPlus C F hF ≤ phiPlus C G hG

The nonzero first factor of one HN filtration cannot have higher phase than the first factor of another filtration of the same object.

theorem CategoryTheory.Triangulated.HNFiltration.phiPlus_eq_of_firstFactors_nonzero (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} (F G : HNFiltration C s.P E) (hF : 0 < F.n) (hG : 0 < G.n) (hneF : ¬Limits.IsZero (F.factor ⟨0, hF⟩)) (hneG : ¬Limits.IsZero (G.factor ⟨0, hG⟩)) : phiPlus C F hF = phiPlus C G hG

Nonzero first factors of two HN filtrations have the same phase.

theorem CategoryTheory.Triangulated.HNFiltration.lastFactor_isZero_of_hom_eq_zero (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} (F : HNFiltration C s.P E) (hn : 0 < F.n) (hzero : ∀ (f : E ⟶ F.factor ⟨F.n - 1, ⋯⟩), f = 0) : Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)

A last factor is zero when every map from the filtered object to it vanishes.

theorem CategoryTheory.Triangulated.HNFiltration.phiMinus_le_of_lastFactor_nonzero (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} (F G : HNFiltration C s.P E) (hF : 0 < F.n) (hG : 0 < G.n) (hneG : ¬Limits.IsZero (G.factor ⟨G.n - 1, ⋯⟩)) : phiMinus C F hF ≤ phiMinus C G hG

The last factor of any HN filtration is bounded above by a nonzero last factor of another filtration of the same object.

theorem CategoryTheory.Triangulated.HNFiltration.phiMinus_eq_of_lastFactors_nonzero (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} (F G : HNFiltration C s.P E) (hF : 0 < F.n) (hG : 0 < G.n) (hneF : ¬Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)) (hneG : ¬Limits.IsZero (G.factor ⟨G.n - 1, ⋯⟩)) : phiMinus C F hF = phiMinus C G hG

Nonzero last factors of two HN filtrations have the same phase.

noncomputable def CategoryTheory.Triangulated.Slicing.phiPlus (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) : ℝ

The intrinsic highest phase of a nonzero object.

Equations

• CategoryTheory.Triangulated.Slicing.phiPlus C s E hE = CategoryTheory.Triangulated.HNFiltration.phiPlus C ⋯.choose ⋯

noncomputable def CategoryTheory.Triangulated.Slicing.phiMinus (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) : ℝ

The intrinsic lowest phase of a nonzero object.

Equations

• CategoryTheory.Triangulated.Slicing.phiMinus C s E hE = CategoryTheory.Triangulated.HNFiltration.phiMinus C ⋯.choose ⋯

theorem CategoryTheory.Triangulated.Slicing.phiPlus_eq (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) (hne : ¬Limits.IsZero (F.factor ⟨0, hn⟩)) : phiPlus C s E hE = HNFiltration.phiPlus C F hn

Any HN filtration with nonzero first factor computes the intrinsic highest phase.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_iso (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 E' : C} (e : E ≅ E') (hE : ¬Limits.IsZero E) (hE' : ¬Limits.IsZero E') : phiPlus C s E hE = phiPlus C s E' hE'

The intrinsic highest phase is invariant under isomorphism.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_eq (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) (hne : ¬Limits.IsZero (F.factor ⟨F.n - 1, ⋯⟩)) : phiMinus C s E hE = HNFiltration.phiMinus C F hn

Any HN filtration with nonzero last factor computes the intrinsic lowest phase.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_iso (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 E' : C} (e : E ≅ E') (hE : ¬Limits.IsZero E) (hE' : ¬Limits.IsZero E') : phiMinus C s E hE = phiMinus C s E' hE'

The intrinsic lowest phase is invariant under isomorphism.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_le_phiPlus (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) : phiMinus C s E hE ≤ phiPlus C s E hE

The intrinsic lowest phase is no greater than the intrinsic highest phase.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_eq_of_semistable (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) (φ : ℝ) (hP : s.P φ E) : phiPlus C s E hE = φ

A nonzero semistable object's intrinsic highest phase is its semistable phase.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_eq_of_semistable (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) (φ : ℝ) (hP : s.P φ E) : phiMinus C s E hE = φ

A nonzero semistable object's intrinsic lowest phase is its semistable phase.

theorem CategoryTheory.Triangulated.Slicing.exists_hn_intrinsic_width (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), HNFiltration.phiPlus C F hn = phiPlus C s E hE ∧ HNFiltration.phiMinus C F hn = phiMinus C s E hE

Some HN filtration realizes both intrinsic phase extrema.