Objects of zero tilted charge

This file owns the degenerate locus of the tilt: zero-charge objects of the tilted heart lie in P(1), the characterisation of that locus, vanishing of maps out of it into a tilted-semistable object, and the semistability of the left endpoint that follows.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.zeroCharge_mem_P_one {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {E : C} (hEheart : (Slicing.toTStructure C sigma.slicing).heart E) (hZ : sigma.Z (v (K₀.of C E)) = 0) : sigma.slicing.P 1 E

A zero-charge object of the original slicing heart belongs to the boundary slice P(1).

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction_zeroCharge_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (E : C) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).zeroCharge E ↔ sigma.zeroCharge E

Rotation and HRS tilting do not change the zero-charge subcategory: the zero-charge objects of the tilted heart are precisely the original-heart objects of zero original charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.hom_eq_zero_of_zeroCharge_to_phaseTiltSemistable {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) {E A0 : C} (hE : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E) (hcharge : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E ≠ 0) (hA0 : sigma.zeroCharge A0) (hrefine : 0 < ((sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E).im ∨ (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsStable E) (f : A0 ⟶ E) : f = 0

The moreover mechanism in Lemma 14.17. A map from an original zero-charge object to a nonzero-charge tilted-semistable object vanishes away from the boundary ray; strict stability gives the same conclusion on the boundary.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_isSemistable_left_of_zeroCharge_right {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) {A E V : C} (hA : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart A) (hV : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart V) (hE : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable E) (hVzero : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).zeroCharge V) {f : A ⟶ E} {g : E ⟶ V} {d : V ⟶ (shiftFunctor C 1).obj A} (hdist : Pretriangulated.Triangle.mk f g d ∈ Pretriangulated.distinguishedTriangles) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).IsSemistable A

A semistable object's subobject with zero-charge quotient is itself semistable. The proof forms the composite subobject in the abelian tilted heart and compares its cokernel charge with the original quotient charge.