Mass and the stability metric under transfer

Lemma 3.5(3) and Lemma 3.9(3) of arXiv:2607.28411v1 compare the generalized distance of two slicings before and after transfer. On stability conditions the metric has a third coordinate, the logarithmic ratio of masses, and it behaves at least as well: the mass of an object for the transferred condition is the mass of its image, because the HN filtration is detected by the functor and the charges agree factor by factor.

Main results

• HNFiltration.mass_mapPreimage and stabilityMass_preimage: the mass of an object for the transferred condition is the mass of its image.
• phiPlusDist_preimage, phiMinusDist_preimage, massDist_preimage: the three coordinates separately, each computed at the image object.
• stabilityDistTerm_preimage: every objectwise three-coordinate term of the transferred conditions is the corresponding term of the originals at the image object.
• stabilityDist_preimage_le: the full three-coordinate distance does not increase under transfer, extending slicingDist_preimage_le.

Implementation notes

stabilityMass is choice-free, a supremum over all HN filtrations, and stabilityMass_eq_mass identifies it with the mass of any one of them. The transfer statement is therefore proved on one filtration of the source object, pushed forward by HNFiltration.mapPreimage, and then lifted to the supremum on both sides.

References

• arXiv:2607.28411v1, Lemmas 3.5(3) and 3.9(3), and the mass m_σ of Definition 2.2.

theorem CategoryTheory.Triangulated.HNFiltration.mass_mapPreimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) {E : C} (Fil : HNFiltration C (σ.slicing.preimage F hσ).P E) : mass σ (mapPreimage σ.slicing F hσ Fil) = mass (σ.preimage F hσ) Fil

The pushed-forward HN filtration has the same mass: its factors are the images of the original factors, and the transferred charge of a factor is the charge of its image.

theorem CategoryTheory.Triangulated.stabilityMass_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (E : C) : stabilityMass (σ.preimage F hσ) E = stabilityMass σ (F.obj E)

Mass is computed on the image. The HN mass of an object for the transferred stability condition equals the HN mass of its image for the original one. This is the mass coordinate behind Lemmas 3.5(3) and 3.9(3) of arXiv:2607.28411v1, which the paper states only for phases.

theorem CategoryTheory.Triangulated.phiPlusDist_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ τ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (hτ : τ.slicing.PreimageData F) (E : C) (hE : ¬Limits.IsZero E) : phiPlusDist (σ.preimage F hσ) (τ.preimage F hτ) E hE = phiPlusDist σ τ (F.obj E) ⋯

The φ⁺ coordinate transports exactly: both φ⁺ values are computed on the image by Slicing.preimage_phiPlus, and the nonvanishing side condition at the image is supplied by Slicing.PreimageData.not_isZero_obj, so no conservativity hypothesis enters.

theorem CategoryTheory.Triangulated.phiMinusDist_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ τ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (hτ : τ.slicing.PreimageData F) (E : C) (hE : ¬Limits.IsZero E) : phiMinusDist (σ.preimage F hσ) (τ.preimage F hτ) E hE = phiMinusDist σ τ (F.obj E) ⋯

The φ⁻ coordinate transports exactly, by Slicing.preimage_phiMinus, mirroring phiPlusDist_preimage.

theorem CategoryTheory.Triangulated.massDist_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ τ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (hτ : τ.slicing.PreimageData F) (E : C) : massDist (σ.preimage F hσ) (τ.preimage F hτ) E = massDist σ τ (F.obj E)

The mass coordinate needs no phase argument at all: stabilityMass_preimage is an equality, so the logarithmic mass discrepancy transports without a ≤, unlike the supremum in stabilityDist_preimage_le.

theorem CategoryTheory.Triangulated.stabilityDistTerm_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ τ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (hτ : τ.slicing.PreimageData F) (E : C) (hE : ¬Limits.IsZero E) : stabilityDistTerm (σ.preimage F hσ) (τ.preimage F hτ) E hE = stabilityDistTerm σ τ (F.obj E) ⋯

The max of the three coordinates transports termwise. This is what makes stabilityDist_preimage_le a comparison of suprema over different index sets rather than an equality: the transferred supremum ranges over the image objects only.

theorem CategoryTheory.Triangulated.stabilityDist_preimage_le {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ τ : StabilityCondition.WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hσ : σ.slicing.PreimageData F) (hτ : τ.slicing.PreimageData F) : stabilityDist (σ.preimage F hσ) (τ.preimage F hτ) ≤ stabilityDist σ τ

Transfer does not increase the stability distance. The transferred supremum runs over the terms of the original one at image objects, so it is bounded by the original supremum. This extends slicingDist_preimage_le, Lemmas 3.5(3) and 3.9(3) of arXiv:2607.28411v1, by the mass coordinate.