The observable stability function on the canonical heart

This file owns the bridge from a stability condition with an arbitrary class map to an ordinary StabilityFunction on its canonical heart. It forgets the presentation lattice, transports the charge, and proves that the resulting heart-level stability function has Harder--Narasimhan filtrations and that its semistable objects are exactly the ambient slicing's.

Only this bridge lives here. Mass estimates along distinguished triangles are developed in the sibling modules and consume this file through the umbrella.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observable {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) : StabilityCondition C

Forget the presentation lattice while retaining the observable charge on K₀(C). This is composition of additive homomorphisms, not an operation on stability conditions. It lets the ordinary heart-equivalence API be reused for a condition defined with an arbitrary class map.

Equations

• σ.observable = { toWithClassMap := CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ofStrict σ.slicing (σ.Z.comp v) ⋯, locallyFinite := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observable_slicing {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) : σ.observable.slicing = σ.slicing

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observable_charge {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : C) : σ.observable.charge E = σ.charge E

noncomputable def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) : StabilityFunction (Slicing.toTStructure C σ.slicing).heart.FullSubcategory

The heart stability function associated to a class-map stability condition, obtained from its observable ordinary stability condition.

Equations

• σ.observableStabilityFunctionOnHeart = { Z := σ.Z.comp (v.comp (CategoryTheory.K₀Ab.toAmbient (CategoryTheory.Triangulated.Slicing.toTStructure C σ.slicing))), nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart_charge {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) : σ.observableStabilityFunctionOnHeart.charge E = σ.charge E.obj

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart_phase_eq_of_mem_P {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) (E : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hP : σ.slicing.P φ E.obj) (hE : ¬Limits.IsZero E) : σ.observableStabilityFunctionOnHeart.phase E = φ

On a nonzero heart object already lying in a slice, the phase of the restricted owner stability function is that slice parameter.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart_phase_le_phiPlus {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hE : ¬Limits.IsZero E) : σ.observableStabilityFunctionOnHeart.phase E ≤ Slicing.phiPlus C σ.slicing E.obj ⋯

The heart phase is bounded by the highest ambient HN phase. The non-boundary case is the owner weak-charge argument bound; at phase one the claim follows from the intrinsic range of an abelian stability phase.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart_isSemistable_of_mem_P {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) (E : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hP : σ.slicing.P φ E.obj) (hE : ¬Limits.IsZero E) : σ.observableStabilityFunctionOnHeart.IsSemistable E

Ambient slice semistability implies semistability for the restricted owner stability function on the canonical heart.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.observableStabilityFunctionOnHeart_hasHN {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) : σ.observableStabilityFunctionOnHeart.HasHNProperty

The observable heart stability function has Harder--Narasimhan filtrations.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.mem_slicing_of_heart_isSemistable {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hE : σ.observableStabilityFunctionOnHeart.IsSemistable E) : σ.slicing.P (σ.observableStabilityFunctionOnHeart.phase E) E.obj

The converse half of the heart/slicing semistability comparison. A nonzero object that is semistable for the stability function on the canonical heart is semistable in the ambient slicing, at the same phase.