Weak stability on the heart of a slicing

This file is the semistable-object part of the weak heart--slicing correspondence from Lemma 14.4 of arXiv:1902.08184v4. A weak prestability condition restricts to a weak stability function on its slicing heart. The only new boundary case relative to the ordinary construction is phase 1: compatibility permits a zero radius there, and therefore the induced heart charge lands on the closed negative real ray.

The main declarations are:

• WeakPreStabilityCondition.weakStabilityFunctionOnHeart;
• charge and zero-charge compatibility for that restriction;
• Slicing.phiPlus_le_of_heart_subobject, the triangle-form heart-mono bridge;
• weakStabilityFunctionOnHeart_isSemistable_iff, identifying slicing and slope semistability for nonzero slicing-heart objects.

The analytic proof splits at phase 1. Below 1, every nonzero HN factor has strictly positive radius and the ordinary argument-convexity API applies. At phase 1, additivity and the closed half-plane force both ends of every heart short exact sequence to have zero imaginary part, hence slope +infinity.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) : WeakStabilityFunction (Slicing.toTStructure C σ.slicing)

Restrict a weak prestability condition to its slicing heart.

Equations

• σ.weakStabilityFunctionOnHeart = { Z := σ.Z.comp v, nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_Z {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) : σ.weakStabilityFunctionOnHeart.Z = σ.Z.comp v

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_charge {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) : σ.weakStabilityFunctionOnHeart.charge E = σ.Z (v (K₀.of C E))

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) : σ.weakStabilityFunctionOnHeart.zeroCharge E ↔ (Slicing.toTStructure C σ.slicing).heart E ∧ σ.Z (v (K₀.of C E)) = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.SlicingBridge.phiPlus_le_of_heart_subobject {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] (s : Slicing C) {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) {E A B : C} (hP : s.P phi E) (hAheart : (Slicing.toTStructure C s).heart A) (hBheart : (Slicing.toTStructure C s).heart B) (hA : ¬Limits.IsZero A) {f : A ⟶ E} {g : E ⟶ B} {d : B ⟶ (shiftFunctor C 1).obj A} (hdist : Pretriangulated.Triangle.mk f g d ∈ Pretriangulated.distinguishedTriangles) : Slicing.phiPlus C s A hA ≤ phi

A heart subobject of a slicing-semistable object has top HN phase at most the phase of the ambient object. The subobject is presented by a distinguished triangle whose three vertices lie in the slicing heart.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.charge_mem_upperHalfPlane_and_arg_le_phiPlus {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) (hheart : (Slicing.toTStructure C σ.slicing).heart E) (hE : ¬Limits.IsZero E) (hplus : Slicing.phiPlus C σ.slicing E hE < 1) : σ.weakStabilityFunctionOnHeart.charge E ∈ semiClosedUpperHalfPlane ∧ (σ.weakStabilityFunctionOnHeart.charge E).arg ≤ Real.pi * Slicing.phiPlus C σ.slicing E hE

Below the boundary phase, the induced weak charge is nonzero and its argument is bounded above by the largest slicing HN phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.pi_mul_phiMinus_le_charge_arg_of_im_pos {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) (hheart : (Slicing.toTStructure C σ.slicing).heart E) (hE : ¬Limits.IsZero E) (him : 0 < (σ.weakStabilityFunctionOnHeart.charge E).im) : Real.pi * Slicing.phiMinus C σ.slicing E hE ≤ (σ.weakStabilityFunctionOnHeart.charge E).arg

If the induced weak charge has positive imaginary part, its argument is bounded below by the smallest slicing HN phase. Zero-charge phase-1 factors are discarded from the sum; positive imaginary part guarantees that at least one charged factor remains.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_isSemistable_of_mem_P_phi {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) (E : C) (hP : σ.slicing.P phi E) (hE : ¬Limits.IsZero E) : σ.weakStabilityFunctionOnHeart.IsSemistable E

Slicing ray membership in (0,1] implies slope semistability for the induced weak stability function on the slicing heart.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.mem_P_phiPlus_of_weakStabilityFunctionOnHeart_isSemistable {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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) (hE : ¬Limits.IsZero E) (hss : σ.weakStabilityFunctionOnHeart.IsSemistable E) : σ.slicing.P (Slicing.phiPlus C σ.slicing E hE) E

A nonzero heart object that is slope-semistable for the induced weak stability function lies in the slicing at its intrinsic top phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_isSemistable_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] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) (hheart : (Slicing.toTStructure C σ.slicing).heart E) (hE : ¬Limits.IsZero E) : σ.weakStabilityFunctionOnHeart.IsSemistable E ↔ σ.slicing.P (Slicing.phiPlus C σ.slicing E hE) E

For nonzero heart objects, slicing semistability and semistability for the induced weak stability function are equivalent.