The lifted linear action on slicings #
A normalized shift f acts on a slicing by relabelling phases:
(f • s).P φ = s.P (f⁻¹ φ)
f⁻¹ rather than f is what makes this a left action, and mul_smul
below is the test that pins it down — with f in place of f⁻¹ the
definition still typechecks and mul_smul fails.
Only the NormalizedShift factor is involved: the matrix factor of
G̃L⁺(2, ℝ) acts on the central charge, not on the slicing. So the action is
defined for NormalizedShift and GLTilde inherits it through
GLTilde.toShiftHom.
Why the axioms survive #
The axiom with content is shift_iff, which needs
f⁻¹ (φ + 1) = f⁻¹ φ + 1 — i.e. exactly
NormalizedShift.symm_map_add_one, here reached through the group structure
as f⁻¹.map_add_one.
hn_exists reuses the Postnikov tower untouched — PostnikovTower carries no
phase data, all of it lives in HNFiltration's extra fields — and relabels
the factor phases by f.
Relabel a slicing's phases by f: the objects semistable of phase φ in
relabel f s are those semistable of phase f⁻¹ φ in s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalized shifts act on slicings by phase relabelling.
Equations
- One or more equations did not get rendered due to their size.
G̃L⁺(2, ℝ) acts on slicings through its phase-relabelling factor.
The matrix factor is not involved — it acts on the central charge, which is handled by the prestability action.
Equations
- One or more equations did not get rendered due to their size.
Interval subcategories are reindexed, not deformed #
Slicing.intervalProp s a b is "zero, or has an HN filtration with every
phase in (a, b)". Relabelling phases by f therefore just moves the window:
the objects lying in (a, b) for f • s are exactly those lying in
(f⁻¹ a, f⁻¹ b) for s.
The interval subcategories match up on the nose — no equivalence to chase and
no structure to transport — so the remaining obstacle is the shape of the
window, which is what NormalizedShift.exists_radius addresses.