Rotated charge sums along owner filtrations

Rotated imaginary parts are additive along owner Postnikov towers. Strict signs on all nonzero HN factors therefore give a strict sign on the ambient object as soon as one factor is known to be nonzero.

theorem CategoryTheory.Triangulated.rotatedIm_charge_eq_sum (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (W : Λ →+ ℂ) {E : C} (P : PostnikovTower C E) (ψ : ℝ) : WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ E)) ψ = ∑ i : Fin P.n, WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ (P.factor i))) ψ

Rotated imaginary part of a perturbed charge decomposes over an owner Postnikov tower.

theorem CategoryTheory.Triangulated.rotatedIm_charge_neg_of_hn (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (W : Λ →+ ℂ) {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hn : 0 < F.n) (hfirst : ¬Limits.IsZero (F.factor ⟨0, hn⟩)) (ψ : ℝ) (hneg : ∀ (i : Fin F.n), ¬Limits.IsZero (F.factor i) → WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ (F.factor i))) ψ < 0) : WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ E)) ψ < 0

If all nonzero HN factors have negative rotated charge and the first factor is nonzero, then the ambient charge has negative rotated part.

theorem CategoryTheory.Triangulated.rotatedIm_charge_pos_of_hn (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (W : Λ →+ ℂ) {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hn : 0 < F.n) (hfirst : ¬Limits.IsZero (F.factor ⟨0, hn⟩)) (ψ : ℝ) (hpos : ∀ (i : Fin F.n), ¬Limits.IsZero (F.factor i) → 0 < WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ (F.factor i))) ψ) : 0 < WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ E)) ψ

If all nonzero HN factors have positive rotated charge and the first factor is nonzero, then the ambient charge has positive rotated part.

theorem CategoryTheory.Triangulated.Slicing.rotatedIm_charge_neg_of_interval (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (s : Slicing C) (W : Λ →+ ℂ) {E : C} {a b ψ : ℝ} (hI : intervalProp C s a b E) (hE : ¬Limits.IsZero E) (hneg : ∀ (F : C) (φ : ℝ), s.P φ F → ¬Limits.IsZero F → a < φ → φ < b → WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ F)) ψ < 0) : WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ E)) ψ < 0

A nonzero interval object has negative rotated charge when each nonzero semistable factor in the interval does.

theorem CategoryTheory.Triangulated.Slicing.rotatedIm_charge_pos_of_interval (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (s : Slicing C) (W : Λ →+ ℂ) {E : C} {a b ψ : ℝ} (hI : intervalProp C s a b E) (hE : ¬Limits.IsZero E) (hpos : ∀ (F : C) (φ : ℝ), s.P φ F → ¬Limits.IsZero F → a < φ → φ < b → 0 < WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ F)) ψ) : 0 < WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (W (classOf C κ E)) ψ

A nonzero interval object has positive rotated charge when each nonzero semistable factor in the interval does.