Weak heart--slicing equivalence: reverse-direction foundations

This file starts the reverse direction of the weak heart--slicing correspondence. The first reusable ingredient is the order-preserving normalisation of the extended weak slope to a phase in (0, 1]:

mu |-> arctan(mu) / pi + 1 / 2, with +infinity |-> 1.

Unlike the ordinary argument, this definition assigns phase 1 to a zero-charge semistable factor. Its strict monotonicity is the precise bridge which turns the strict WithTop-slope order in WeakAbelianHNFiltration into strict phase order.

The second ingredient converts the subobject chain of a weak abelian HN filtration into an ambient Postnikov tower. This is independent of the eventual analytic central-charge compatibility and is the categorical bridge needed by the reverse construction.

Extended slopes as phases

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope : WithTop ℝ → ℝ

Normalize an extended weak slope to the standard phase interval. The finite branch is the inverse of mu = -cot (pi * phi); the infinite branch is the weak boundary phase 1.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope n = WithTop.recTopCoe 1 (fun (mu : ℝ) => Real.arctan mu / Real.pi + 1 / 2) n

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_top : weakPhaseOfSlope ⊤ = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_coe (mu : ℝ) : weakPhaseOfSlope ↑mu = Real.arctan mu / Real.pi + 1 / 2

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_coe_mem_Ioo (mu : ℝ) : weakPhaseOfSlope ↑mu ∈ Set.Ioo 0 1

Finite slopes have phase strictly between 0 and 1.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_mem_Ioc (mu : WithTop ℝ) : weakPhaseOfSlope mu ∈ Set.Ioc 0 1

Every extended slope has phase in (0, 1].

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_strictMono : StrictMono weakPhaseOfSlope

The slope-to-phase normalization is strictly increasing.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope_lt_iff {mu nu : WithTop ℝ} : weakPhaseOfSlope mu < weakPhaseOfSlope nu ↔ mu < nu

Strict slope order is exactly strict normalized-phase order.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.phase {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) (E : C) : ℝ

Weak phase of a heart object, defined from its extended slope.

Equations

• W.phase E = CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope (W.slope E)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.phase_mem_Ioc {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) (E : C) : W.phase E ∈ Set.Ioc 0 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.phase_lt_phase_iff {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) {E F : C} : W.phase E < W.phase F ↔ W.slope E < W.slope F

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.phase_eq_of_iso {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) {E F : C} (e : E ≅ F) : W.phase E = W.phase F

The heart phase predicate

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heartPhasePredicate {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) (phi : ℝ) : ObjectProperty C

The phase slice determined by a weak stability function on a heart. Zero objects belong to every slice; a nonzero member is weak-semistable and its normalized extended slope is the requested phase.

Equations

• W.heartPhasePredicate phi E = (CategoryTheory.Limits.IsZero E ∨ W.IsSemistable E ∧ W.phase E = phi)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heartPhasePredicate_closedUnderIso {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) (phi : ℝ) : (W.heartPhasePredicate phi).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heartPhasePredicate_instClosedUnderIso {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) (phi : ℝ) : (W.heartPhasePredicate phi).IsClosedUnderIsomorphisms

Integer-normalized ambient phase predicates

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase (phi : ℝ) : ℝ

The representative of a real phase in the standard interval (0, 1].

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase phi = toIocMod CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase._proof_1 0 phi

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex (phi : ℝ) : ℤ

The integral translation carrying phaseBase phi back to phi.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex phi = toIocDiv CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex._proof_1 0 phi

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase_mem (phi : ℝ) : phaseBase phi ∈ Set.Ioc 0 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase_add_phaseIndex (phi : ℝ) : phaseBase phi + ↑(phaseIndex phi) = phi

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase_add_one (phi : ℝ) : phaseBase (phi + 1) = phaseBase phi

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex_add_one (phi : ℝ) : phaseIndex (phi + 1) = phaseIndex phi + 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase_eq_of_mem_Ioc {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) : phaseBase phi = phi

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex_eq_zero_of_mem_Ioc {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) : phaseIndex phi = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex_lt_phase (phi : ℝ) : ↑(phaseIndex phi) < phi

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phase_le_phaseIndex_add_one (phi : ℝ) : phi ≤ ↑(phaseIndex phi) + 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex_le_of_lt {phi₁ phi₂ : ℝ} (h : phi₂ < phi₁) : phaseIndex phi₂ ≤ phaseIndex phi₁

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.shiftedHeartPhasePredicate {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) (psi : ℝ) (n : ℤ) : ObjectProperty C

A weak-semistable heart object of phase psi, shifted into cohomological degree n. The phase normalization functions phaseBase and phaseIndex are shared with the ordinary reverse heart--slicing construction.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate {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) (phi : ℝ) : ObjectProperty C

The ambient phase family induced by a weak stability function on a heart: normalize into (0, 1], then shift by the integral phase index.

Equations

• W.ambientPhasePredicate phi = W.shiftedHeartPhasePredicate (CategoryTheory.Triangulated.WeakStabilityCondition.phaseBase phi) (CategoryTheory.Triangulated.WeakStabilityCondition.phaseIndex phi)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.shiftedHeartPhasePredicate_zero_iff {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) (psi : ℝ) (X : C) : W.shiftedHeartPhasePredicate psi 0 X ↔ W.heartPhasePredicate psi X

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_iff_of_mem_Ioc {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) {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) (X : C) : W.ambientPhasePredicate phi X ↔ W.heartPhasePredicate phi X

On the standard phase interval, the ambient predicate is exactly the heart weak-semistability predicate.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.shiftedHeartPhasePredicate_closedUnderIso {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) (psi : ℝ) (n : ℤ) : (W.shiftedHeartPhasePredicate psi n).IsClosedUnderIsomorphisms

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_closedUnderIso {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) (phi : ℝ) : (W.ambientPhasePredicate phi).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_instClosedUnderIso {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) (phi : ℝ) : (W.ambientPhasePredicate phi).IsClosedUnderIsomorphisms

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.shiftedHeartPhasePredicate_shift_iff {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) (psi : ℝ) (n : ℤ) (X : C) : W.shiftedHeartPhasePredicate psi n X ↔ W.shiftedHeartPhasePredicate psi (n + 1) ((shiftFunctor C 1).obj X)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_shift_iff {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) (phi : ℝ) (X : C) : W.ambientPhasePredicate phi X ↔ W.ambientPhasePredicate (phi + 1) ((shiftFunctor C 1).obj X)

Shifting by [1] raises the normalized ambient weak phase by 1.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_shift_int {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) (phi : ℝ) (X : C) (n : ℤ) : W.ambientPhasePredicate phi X ↔ W.ambientPhasePredicate (phi + ↑n) ((shiftFunctor C n).obj X)

Shifting by an arbitrary integer translates the induced ambient weak phase by that integer. This is the iteration form needed to move HN towers of pure t-cohomology objects to and from the heart.

Abelian HN chains as ambient Postnikov towers

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_3 {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 to form successive cokernels in a weak HN chain.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_3 = t.heartFullSubcategoryAbelian

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factorInclusion {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : Subobject.underlying.obj (F.chain j.castSucc) ⟶ Subobject.underlying.obj (F.chain j.succ)

The inclusion between consecutive terms of a weak abelian HN chain.

Equations

• F.factorInclusion j = (F.chain j.castSucc).ofLE (F.chain j.succ) ⋯

instance CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factorInclusion_mono {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : Mono (F.factorInclusion j)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factorTriangle {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : Pretriangulated.Triangle C

The distinguished triangle attached to one consecutive quotient in a weak abelian HN chain.

Equations

• F.factorTriangle j = CategoryTheory.Pretriangulated.Triangle.mk (F.factorInclusion j).hom (CategoryTheory.Limits.cokernel.π (F.factorInclusion j)).hom (Classical.choose ⋯)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factorTriangle_distinguished {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : F.factorTriangle j ∈ Pretriangulated.distinguishedTriangles

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.toAmbientHN {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) : HNFiltration C W.heartPhasePredicate E.obj

A weak abelian HN filtration gives an ambient HN filtration for the heart phase predicate. Its factors and phases are definitionally the successive cokernels and normalized stored slopes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.HNFiltration.relabelPhasePredicate {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (hsemistable : ∀ (j : Fin F.n), Q (F.φ j) (F.factor j)) : HNFiltration C Q E

Relabel the semistable factors of an HN filtration without changing its underlying Postnikov tower or phase function.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.HNFiltration.relabelPhasePredicate F hsemistable = { toPostnikovTower := F.toPostnikovTower, φ := F.φ, hφ := ⋯, semistable := hsemistable }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.toAmbientNormalizedHN {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 : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) : HNFiltration C W.ambientPhasePredicate E.obj

A weak abelian HN filtration of a heart object is already an ambient HN filtration for the integer-normalized weak phase family.

Equations

• F.toAmbientNormalizedHN = CategoryTheory.Triangulated.WeakStabilityCondition.HNFiltration.relabelPhasePredicate F.toAmbientHN ⋯

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHNOfHeart {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 : W.HasHNProperty) (E : t.heart.FullSubcategory) : HNFiltration C W.ambientPhasePredicate E.obj

Heart-level weak HN existence supplies ambient HN towers for every object of that heart. Zero heart objects use the empty tower.

Equations

• W.ambientHNOfHeart hHN E = if hE : CategoryTheory.Limits.IsZero E then CategoryTheory.Triangulated.HNFiltration.zero C E.obj ⋯ else (Classical.choice ⋯).toAmbientNormalizedHN

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientHN_exists_of_mem_heart {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 : W.HasHNProperty) (E : C) (hE : t.heart E) : Nonempty (HNFiltration C W.ambientPhasePredicate E)

Packaging the reverse construction

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ReverseSlicingObligations {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) : Prop

The two genuinely ambient obligations left after constructing weak phase slices from heart data. Heart-level HN gives the required towers on the heart by ambientHN_exists_of_mem_heart; this package asks only for their extension to all shifts and finite cohomological extensions, together with Hom vanishing.

• hom_vanishing (phi₁ phi₂ : ℝ) (A B : C) : phi₂ < phi₁ → W.ambientPhasePredicate phi₁ A → W.ambientPhasePredicate phi₂ B → ∀ (f : A ⟶ B), f = 0

  Morphisms from a higher weak phase to a lower one vanish.

• hn_exists (E : C) : Nonempty (HNFiltration C W.ambientPhasePredicate E)

  Every ambient object admits an HN filtration for the induced phases.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ReverseSlicingObligations.toSlicing {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} (O : W.ReverseSlicingObligations) : Slicing C

Construct the ambient slicing determined by a heart weak stability function once its two ambient reverse obligations have been discharged.

Equations

• O.toSlicing = { P := W.ambientPhasePredicate, closedUnderIso := ⋯, zero_mem := ⋯, shift_iff := ⋯, hom_vanishing := ⋯, hn_exists := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ReverseSlicingObligations.toSlicing_P {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} (O : W.ReverseSlicingObligations) : O.toSlicing.P = W.ambientPhasePredicate

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ReverseSlicingObligations.toWeakPreStabilityCondition {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {t : TStructure C} {W : WeakStabilityFunction t} {v : K₀ C →+ Λ} (O : W.ReverseSlicingObligations) (Z : Λ →+ ℂ) (compat : ∀ (phi : ℝ) (E : C), W.ambientPhasePredicate phi E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), phi ≠ ↑n) → 0 < m) ∧ Z (v (K₀.of C E)) = ↑m * Complex.exp (↑Real.pi * ↑phi * Complex.I)) : WeakPreStabilityCondition v

Package the reverse slicing as a weak prestability condition. The remaining compat premise is deliberately stated in Definition 14.1's ray language; the slope--phase analytic bridge discharges it independently of the categorical HN assembly.

Equations

• O.toWeakPreStabilityCondition Z compat = { slicing := O.toSlicing, Z := Z, compat' := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ReverseSlicingObligations.toWeakPreStabilityCondition_slicing {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {t : TStructure C} {W : WeakStabilityFunction t} {v : K₀ C →+ Λ} (O : W.ReverseSlicingObligations) (Z : Λ →+ ℂ) (compat : ∀ (phi : ℝ) (E : C), W.ambientPhasePredicate phi E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), phi ≠ ↑n) → 0 < m) ∧ Z (v (K₀.of C E)) = ↑m * Complex.exp (↑Real.pi * ↑phi * Complex.I)) : (O.toWeakPreStabilityCondition Z compat).slicing = O.toSlicing