Topology induced by the full stability distance #
This file is the topology-comparison part of Bridgeland's Proposition 8.1.
There is already a topology on StabilityCondition.WithClassMap C v: the
Section 6 topology generated by basisNhd. Consequently it would be unsafe
to install a raw EMetricSpace whose inherited topology might be a second,
merely propositionally equal instance.
The constructor below instead uses
PseudoEMetricSpace.ofEDistOfTopology. Its input is precisely the remaining
interface at this layer: full-distance balls form a neighbourhood basis for
the existing Section 6 topology. The completed mass-subadditivity module
later inhabits that interface as stabilityDistanceTopologyCompatible.
Mathlib then constructs the compatible
uniformity while retaining that topology definitionally. No metric instance
is installed by either module.
The first part of the file records elimination lemmas for a strict full-
distance bound. They feed the easy direction only —
exists_stabilityDist_ball_subset_basisNhd. The hard direction,
exists_basisNhd_subset_stabilityDist_ball, goes through
phiPlus_sub_lt_of_slicingDist
(WeakStabilityCondition/StabilityCondition/Foundation/Deformation/SlicingDistance.lean) and
abs_log_mass_ratio_le_of_mem_basisNhd, and touches none of them.
A strict full-distance bound controls the positive intrinsic phase of every nonzero object.
A strict full-distance bound controls the negative intrinsic phase of every nonzero object.
A strict full-distance bound controls the literal logarithmic mass ratio of every nonzero object.
Exponential form of the mass-coordinate bound.
A full-distance bound gives the convenient one-sided mass comparison.
The preceding mass comparison in the reverse orientation.
Points on the phase unit circle are Lipschitz in their real phase, with
constant π. The exponent convention is the one used by a stability
condition's compatibility axiom.
The charge of a semistable object is its real HN mass times the unit ray at its phase.
If E is σ-semistable of phase φ and the full distance from σ to
τ is less than ε, then the τ-charge of E is close to the ray at φ.
The coefficient on that ray is the full τ-HN mass of E.
This is the finite-HN-sector estimate needed for the easy direction of Proposition 8.1.
A narrow HN sector bounds mass by the norm of the total charge. This is
the mass-specialized lower-sector estimate, used by the hard direction of
the topology comparison (exists_basisNhd_subset_stabilityDist_ball) only.
A pointwise bound on a charge homomorphism over semistable factors extends to every object whose HN phases lie in a sector of width less than one.
A Section 6 basis bound controls the mass of a σ-semistable object in
the nearby stability condition.
The same basis bound controls the old mass of a τ-semistable object in
terms of its new mass. The factor is written so that it tends to one as the
basis radius tends to zero.
The remaining categorical mass lemma needed by the global topology comparison: HN mass is subadditive across every distinguished triangle.
This is stated as a proposition so that all analytic and topological parts of Proposition 8.1 can be checked independently of its filtration-assembly proof. No instance or theorem below assumes it globally without taking an explicit proof argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Real mass is invariant under object isomorphism.
Triangle subadditivity iterated along the first k stages of a Postnikov
tower.
Triangle subadditivity bounds the mass of the top of any Postnikov tower by the sum of the masses of its factors.
With triangle subadditivity, the local semistable estimate extends to all objects.
The global mass comparison in the reverse orientation.
A symmetric logarithmic mass-error coefficient for a Section 6 basis neighborhood.
Equations
Instances For
The two global mass comparisons give a symmetric logarithmic ratio bound.
The symmetric mass-error coefficient tends to zero at the origin, so it can be made smaller than any positive target while retaining the Section 6 radius restrictions.
Assuming triangle subadditivity of mass, every sufficiently small Section 6 basis neighborhood lies in any prescribed positive real full-distance ball. This is the hard cofinality direction of Proposition 8.1.
A convenient uniform charge-error coefficient. It tends to zero with
ε; the first term is angular error and the second is radial mass error.
Equations
Instances For
On a σ-semistable object, a strict full-distance bound controls the
relative difference of the central charges.
A full-distance ball gives a uniform bound in the Section 6 charge seminorm.
The charge-error coefficient can be made smaller than any prescribed positive number while also keeping the distance radius below a prescribed positive radius.
Every centered Section 6 basis neighborhood contains a centered full-
distance ball. This is one of the two cofinality directions in Proposition
8.1, and the one that is unconditional — it does not take
StabilityMassTriangleInequality.
hε8 : ε < 1 / 8 is stronger than this proof needs: it is consumed once, to
derive hε1 : ε < 1 for Real.sin_pos_of_pos_of_lt_pi. It is kept because
ε < 1/8 is the radius convention of the whole basisNhd family
(WeakStabilityCondition/StabilityCondition/Foundation/Deformation/StabilityTopology.lean) and
matches basisNhdFamily's generating predicate; weakening it here alone would
desynchronise this lemma from its siblings for no gain.
The centered Section 6 neighborhoods are a neighborhood basis for the already installed topology.
The exact compatibility statement needed to turn stabilityDist into
Mathlib's extended metric without changing the already installed Section 6
topology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Once mass subadditivity across distinguished triangles is supplied, the
full-distance balls form a basis for the existing Section 6 topology. This
packages both cofinality directions and is the exact hypothesis consumed by
PseudoEMetricSpace.ofEDistOfTopology.
The compatible pseudo-extended-metric structure, constructed from the
existing topology. This is deliberately a named definition, not an instance:
the instance is installed only after StabilityDistanceTopologyCompatible is
proved.
Equations
Instances For
Regression check for the instance-diamond issue: the topology inherited from the compatible pseudo-extended metric is definitionally the Section 6 topology that was already present on stability conditions.
The extended distance field of the compatible structure is literally
stabilityDist; no coercion or replacement distance is introduced.
With a surjective class map, separation upgrades the compatible pseudo-extended metric to an extended metric. As above this remains a named definition until the topology comparison is closed.
Equations
- CategoryTheory.Triangulated.stabilityEMetricSpace hv hcompat = { toPseudoEMetricSpace := CategoryTheory.Triangulated.stabilityPseudoEMetricSpace hcompat, eq_of_edist_eq_zero := ⋯ }
Instances For
The separated extended-metric upgrade retains the same definitionally compatible topology.
Mass-premise-parameterized end-to-end pseudo-extended-metric package. Its topology is
definitionally the pre-existing Section 6 topology because it is routed
through stabilityPseudoEMetricSpace, not through a fresh metric topology.
Equations
Instances For
Mass-premise-parameterized end-to-end extended-metric package for a surjective class map. The completed mass-subadditivity module supplies the premise; no global instance is installed.