Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Weak.Heart.HomVanishing

Hom vanishing for weak heart phases #

This file discharges the Hom-vanishing half of the reverse weak heart--slicing construction. The key new ingredient is a weak-slope see-saw for short exact sequences in the heart. It treats the extended value ⊤ explicitly: a nonzero heart object has slope ⊤ exactly on the closed real boundary of the weak upper half-plane.

The see-saw feeds the standard kernel/image argument. A nonzero morphism between weak-semistable heart objects forces the source slope to be at most the image slope and the image slope to be at most the target slope. Hence a morphism from strictly higher phase to strictly lower phase vanishes. The integer-normalized ambient statement then follows by shifting both objects to the heart when their phase indices agree, and by t-structure orthogonality when the indices differ.

Weak-slope see-saw #

source
theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.slope_between_of_triangle {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {A B Q : C} (hA : t.heart A) (hQ : t.heart Q) (hA0 : ¬Limits.IsZero A) (hQ0 : ¬Limits.IsZero Q) {f : A ⟶ B} {g : B ⟶ Q} {d : Q ⟶ (shiftFunctor C 1).obj A} (hdist : Pretriangulated.Triangle.mk f g d ∈ Pretriangulated.distinguishedTriangles) (hslope : W.slope A ≤ W.slope Q) :
W.slope A ≤ W.slope B ∧ W.slope B ≤ W.slope Q

If the two ends of a heart triangle have ordered weak slopes, the middle slope lies between them. The four cases distinguish positive from vanishing imaginary part at each end; the latter is the extended slope ⊤.

Kernel and image bounds in the heart #

source
@[implicit_reducible]
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.instAbelianFullSubcategoryHeart {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} :
Abelian t.heart.FullSubcategory

The abelian structure on the full heart used for kernels and images.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.slope_le_of_heart_epi {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E Q : t.heart.FullSubcategory} (p : E ⟶ Q) [Epi p] (hE : W.IsSemistable E.obj) (hQ : ¬Limits.IsZero Q) :
    W.slope E.obj ≤ W.slope Q.obj

    Every nonzero quotient of a weak-semistable heart object has slope at least the slope of the source.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heart_subobject_slope_le {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {I F : t.heart.FullSubcategory} (i : I ⟶ F) [Mono i] (hF : W.IsSemistable F.obj) (hI : ¬Limits.IsZero I) :
    W.slope I.obj ≤ W.slope F.obj

    Every nonzero subobject of a weak-semistable heart object has slope at most the slope of the target.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heart_hom_zero_of_semistable_phase_gt {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E F : t.heart.FullSubcategory} (hE : W.IsSemistable E.obj) (hF : W.IsSemistable F.obj) (hphase : W.phase F.obj < W.phase E.obj) (f : E ⟶ F) :
    f = 0

    Hom vanishing for weak-semistable objects in the same heart: a morphism from strictly higher normalized weak phase to lower phase is zero.

    Ambient integer-normalized Hom vanishing #

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_hom_zero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {phi₁ phi₂ : ℝ} {E F : C} (hE : W.ambientPhasePredicate phi₁ E) (hF : W.ambientPhasePredicate phi₂ F) (hgap : phi₂ < phi₁) (f : E ⟶ F) :
    f = 0

    Hom vanishing for the ambient phase predicates induced from a weak stability function on a heart. Equal phase indices reduce to the heart image argument; distinct indices reduce to t-structure orthogonality.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.reverseSlicingObligationsOfHN {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (hHN : ∀ (E : C), Nonempty (HNFiltration C W.ambientPhasePredicate E)) :
    W.ReverseSlicingObligations

    Once ambient HN existence is supplied, Hom vanishing no longer needs to be an independent reverse-slicing premise.