The Aut action preserves the phase distance #
Lemma 8.2 says Aut(D) acts on Stab(D) by isometries. This module proves
the phase half of that clause, and is deliberate about which half it is.
The distance it uses is slicingDist
(WeakStabilityCondition/StabilityCondition/Foundation/Deformation/SlicingDistance.lean), built for
the deformation theory of §7 and not, on its own, the §8 metric.
slicingDist C s₁ s₂ = ⨆ (E : C) (_ : ¬IsZero E),
ENNReal.ofReal (max |φ⁺₁ E - φ⁺₂ E| |φ⁻₁ E - φ⁻₂ E|)
mapEquiv_slicingDist proves the action preserves it, on the nose and with no
finiteness hypothesis. Both sides may be ⊤; the equality still holds.
This is not Bridgeland's d, and the gap is not a technicality #
d(σ₁, σ₂) is a supremum of three quantities. slicingDist carries two of
them — the φ⁺ and φ⁻ discrepancies — and omits
|log (m_{σ₂}(E) / m_{σ₁}(E))|, the mass ratio. The omitted term is the only
one that sees the central charge, and therefore the only one that could move
under Φ at all, since actStabAut replaces Z by Z ∘ lam.
This module itself does not close it: the slicing foundation has no mass
function — m_σ(E) = Σ|Z(A_i)| over the HN factors is not defined anywhere
under Foundation/. The downstream Metric/Mass/Basic.lean,
Metric/Mass/Uniqueness.lean, Metric/Distance/Basic.lean, and
Metric/Isometry/Full.lean define the HN mass, prove independence from the
chosen filtration and finiteness, and prove preservation of the resulting
three-coordinate distance.
So the relation to Lemma 8.2 is no_claim, not one_way, and the reason is a
genuine non-implication rather than modesty. A sup of three terms being
preserved does not give that each term is preserved, so the paper's statement
does not imply this one; and this one plainly does not imply the paper's.
The same call, for the same reason, as gltildeSlicingMulAction.
Why the supremum is bounded twice rather than reindexed #
The obvious proof — reindex the supremum along Φ — does not typecheck, and
the reason is worth keeping. Φ.functor.obj is a function on the object
type of C, and an equivalence of categories makes it injective only up to
isomorphism. Two distinct terms of the type C can be isomorphic objects, and
Φ.functor.obj is free to identify them. There is no Equiv to rewrite along.
What is true is that each side dominates the other pointwise, which is all a
supremum needs. ≤ sends E to Φ⁻¹ E; ≥ sends E to Φ E and then needs
phiPlus_congr to move back along the unit isomorphism. That last step is why
phiPlus_congr exists at all.
The intrinsic phases are invariant under isomorphism of the object #
The deformation modules need this repeatedly and never state it —
Foundation/Deformation/PhaseConfinement.lean and its neighbours inline the
HNFiltration.ofIso argument instead. Stated once here, because the ≥ half
of the isometry cannot be written without it.
φ⁺ depends on the object only up to isomorphism.
φ⁻ depends on the object only up to isomorphism.
An equivalence neither creates nor destroys the zero object #
Both directions are needed: ≤ moves a nonzero E to a nonzero Φ⁻¹ E, and
≥ moves it to a nonzero Φ E. Neither is Functor.map_isZero, which only
goes one way.
Φ⁻¹ E is zero exactly when E is.
Φ E is zero exactly when E is.
The phases transport along the action #
Slicing.mapEquiv moves objects and fixes phases, so φ⁺ of the moved slicing
at E is φ⁺ of the original at Φ⁻¹ E, exactly — no ε, no continuity.
Contrast relabel, where a phase relabelling f sends φ⁺ to f φ⁺ and the
distance is not preserved at all.
φ⁺_{Φ · s}(E) = φ⁺_s(Φ⁻¹ E).
φ⁻_{Φ · s}(E) = φ⁻_s(Φ⁻¹ E).
The isometry #
The Aut action preserves slicingDist. The phase half of Lemma 8.2's
isometry clause.
No finiteness hypothesis: both sides live in ℝ≥0∞ and the equality holds when
they are ⊤.
On stability conditions #
mapEquiv_slicingDist is about slicings. These two carry it to the objects §8
is actually about — first for actStabAut, the general map, then for the
MulAction of AutPairQuot v, which is as close to "the group acts by
isometries" as this repo gets.
Both are one-liners, and that is the point: the content is all in
mapEquiv_slicingDist, and the acted slicing is definitionally
σ.slicing.mapEquiv Φ in both packagings.
actStabAut preserves the phase distance between the underlying slicings.
Note what does not appear on either side: lam. The class-lattice datum
moves the central charge and nothing else, and slicingDist does not see the
central charge — which is exactly why the mass term, which does, is out of
scope here.
The group acts by phase isometries. Every element of AutPairQuot v
preserves slicingDist on the underlying slicings.
_root_.Quotient.inductionOn is safe here without a well-definedness side goal: the
statement is an equation between two ℝ≥0∞s, so it is a Prop and proof
irrelevance discharges the descent.