Transporting stability conditions by autoequivalences #
The assembly step. G̃L⁺(2, ℝ) moves phases and fixes objects; an
autoequivalence does the opposite, and this file carries it all the way to
StabilityCondition.WithClassMap.
Three things had to line up, and each is the dual of the corresponding step
in the G̃L⁺(2, ℝ) track:
- Slicing —
Slicing.mapEquiv(WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Slicing/Transport.lean), dual torelabel. - Local finiteness —
mapEquiv_isLocallyFinitebelow. Dual torelabel_isLocallyFinite, but easier: the interval endpoints do not move (mapEquiv_intervalProp_iff), so the sameηworks and no uniform-continuity argument is needed. What is needed instead is thatΦ⁻¹restricts to a full faithful strict-mono-preserving functor between the two interval categories. - Central charge —
actStabAutbelow, via a class-lattice datumlam.
How strict monos survive Φ⁻¹ #
autFunctor_strictMono uses the cone route, not the heart route: take a
strict mono's cokernel triangle
(interval_strictShortExact_cokernel_of_strictMono then
exists_distTriang_of_strictShortExact), push it through Φ⁻¹ — which is
triangulated, so the triangle stays distinguished and all three vertices stay
in the same window — then read the strict mono back off with
strictMono_strictEpi_of_distTriang. This is exactly how
intervalInclusion_map_strictMono
(WeakStabilityCondition/StabilityCondition/Foundation/Slicing/IntervalFiniteTransfer.lean) works.
The heart route would not have worked: toRightHeart lands in the heart of
phaseShift C (b - 1), and the two slicings' hearts are different
subcategories of C.
The class-lattice datum #
An autoequivalence acts on WithClassMap C v only together with a
lam : Λ →+ Λ satisfying v ∘ K₀.map Φ⁻¹ = lam ∘ v. That is not a
technicality — v is arbitrary, and nothing forces Φ to respect it. When
v = id the datum is forced (lam = K₀.map Φ⁻¹); in general it is extra
input, structurally exactly as Compatible is for GLTilde.
With it, compat' costs nothing: the witness m is unchanged, because Φ
moves the object but not its phase. Contrast the G̃L⁺(2, ℝ) case, where the
matrix rescales the ray and m becomes m * r.
What this is NOT — and what became of that #
This file gives the action as a well-defined map plus its defining
property, not a group action. The acting object is a pair (Φ, lam), and
AutQuot groups the Φs alone — enough for slicings, not once a class lattice
is in play.
WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Stability/ClassMap.lean bundles the pair and supplies the MulAction. Nothing
here is superseded by it, and the split is worth keeping: that file needs
lam : Λ ≃+ Λ, because a group needs lam⁻¹ and nothing produces one, while
actStabAut below asks only for lam : Λ →+ Λ. A non-invertible compatible
datum still acts as a map and is simply not a member of that group, so this
statement is strictly the more general of the two.
See the stability-foundation ownership record in notes/dependencies/.
Φ⁻¹ between interval categories #
Φ⁻¹ restricted to interval subcategories. The endpoints are unchanged —
that is mapEquiv_intervalProp_iff.
An abbrev deliberately: instance search must see through it to find the
Full/Faithful instances of the underlying ObjectProperty.lift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strict monos survive Φ⁻¹, by the cone route.
The restricted inverse autoequivalence sends intrinsic admissible subobjects to intrinsic admissible subobjects.
Local finiteness #
Local finiteness survives an autoequivalence, with the SAME radius.
Dual to relabel_isLocallyFinite and strictly easier: the windows do not move,
so exists_radius is not needed. The content is instead the strict-finite-length
transfer along Φ⁻¹.
The action #
The Aut action on stability conditions.
Φ moves the objects; lam carries it on the class lattice. The witness m
in compat' is unchanged — an autoequivalence moves an object without
moving its phase.
Equations
- One or more equations did not get rendered due to their size.