Charge-zero loci and their connected components in the stability space #
For a stability condition σ : StabilityCondition.WithClassMap C v and a
class δ : Λ, this file defines the locus on which the central charge kills
δ. A regular locus avoids the zero loci indexed by a chosen set Δ, and a
ChargeChamber is a connected component of that regular-locus subtype.
Distinction from the numerical loci #
The locus here is the charge-vanishing locus in the stability space:
chargeZeroLocus δ = {σ | σ.Z δ = 0}.
It is not Wall.Spherical.signedRayRegularLocus, a subset of V × V in the
exp(β + iω) chart cut out by real half-spaces indexed by
sphericalPlus. It is not the tilt-stability construction in
Walls/Numerical/Basic.lean, whose parameter space is the (s, t) half-plane
and whose walls are conics. It is also not PeriodDomain.orthogonalityLocus, whose points
are submodules of a quadratic space and whose locus condition is orthogonality
to a class.
The comparison with the generic ChargeFamily.zeroLocus is explicit through
stabilityChargeFamily. No map from the stability space to either the
spherical chart or the positive-plane carrier is defined here.
Topological boundary #
Only the already-installed topology on StabilityCondition.WithClassMap C v
and the induced subtype topology are used to form ConnectedComponents.
Nothing here proves that chargeZeroLocus is closed or that chargeRegularLocus is open.
Until such a theorem is supplied, a ChargeChamber is the connected component
of a possibly non-open subspace and should not be read as a chamber in the
geometric sense.
Charge-zero loci and their complement #
The central charges carried by the stability space, exposed through the generic family API. This is the comparison map from stability conditions to the upstream charge-zero-locus construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The locus of stability conditions whose central charge kills δ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stability-space charge-zero locus is exactly the generic family zero
locus after applying stabilityChargeFamily.
Membership in chargeZeroLocus δ is vanishing of the charge at δ.
The stability conditions whose central charge is nonzero on every class
in Δ.
Equations
Instances For
Membership in chargeRegularLocus Δ is nonvanishing on every class of Δ.
Enlarging the indexing set can only shrink the regular locus.
Avoiding the charge-zero loci of every lattice class is impossible because the zero class has zero charge.
The regular locus is the complement of the union of its charge-zero loci.
Equivariance #
The combined symmetry sends the charge-zero locus indexed by p.2.lam δ to the locus
indexed by δ.
A combined symmetry maps the charge-zero locus indexed by the transformed class exactly onto the original locus.
The GLTilde action preserves every charge-zero locus setwise.
If the lattice part of a combined symmetry preserves Δ, membership in
the corresponding regular locus is invariant.
If the lattice part of a combined symmetry preserves Δ, the symmetry
preserves the regular locus setwise.
Chambers #
A chamber is a connected component of the regular-locus subtype.
No openness of that subtype is asserted here; see the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chamber containing a point of the regular locus.