Every fixed-u slice of a divisorial alignmentLocus family is an (s, t) half plane #
Walls/Numerical/Basic.lean proves that a numerical alignmentLocus in the (s, t) plane
is a circle centred on the s-axis or a vertical line, that two walls of a
fixed class are disjoint, and that they are nested. Those are theorems about
the three-coordinate polynomial and, until this file, were available only to
the compressed Picard-rank-one transport that geometric consumers build.
The divisorial family of Slice.lean is indexed by
B = s H + G(u), omega = t H with u in an arbitrary real transverse space.
Fixing u and letting (s, t) vary gives a half plane, and the theorem below
says that half plane is the (s, t) model, pulled back along the
degree-weighted triple of the G(u)-twisted character:
(T.chargeFamily ch).reindex (fun (s,t) => ⟨s, u, t⟩)
= stChargeFamily.pullback ((ch.twist S (G u)).coordinatesAt S H).toNumClassHom
Consequently the circle, line, disjointness, and nesting results hold on every
u-slice of a surface of arbitrary Picard rank. This is the alignmentLocus picture used
by Maciocia (arXiv:1202.4587, Prop. 2.6 and Thm 3.1), Arcara--Miles
(arXiv:1401.6149, §4) and Mizuno--Yoshida (arXiv:2502.18894, Thm 2.1), and it is
the reason those papers fix a transverse direction before drawing circles.
The u-dependence is real #
Twisting by G(u) does not change the compressed degree, because H · G(u) = 0,
but it does change the compressed ch₂ and hence the discriminant:
discr of the slice class exceeds the untwisted one by
2 H² r (G(u) · ch₁) - H² r² G(u)² (discr_sliceCoordinates). So the walls
genuinely move as u varies, which is what makes the transverse parameter worth
carrying; only within one u-plane are they nested.
Nesting needs a nonnegative discriminant, and now has one #
barDiscriminant_parameters computes the \bar Δ^B_ω of
Discriminant.lean at a slice point: it is t² times the slice
discriminant, with the s-dependence cancelling exactly. Bogomolov--Gieseker
and a Hodge index at omega therefore discharge the 0 ≤ discr hypothesis of
the disjointness and nesting theorems on every u-plane, not only on the
rank-one one.
Nothing here proves a Bogomolov inequality or a Hodge index theorem; both remain
supplied certificates: DivisorSpace.HodgeIndex here, and a Bogomolov
inequality that only a geometric consumer can provide.
Compressed coordinates as a point of the (s, t) alignmentLocus plane #
The degree-weighted numerical triple of compressed charge coordinates.
The rank slot carries ∫H², which is what the (s,t) charge polynomial
requires; stCharge_toNumClass below is the identity that forces it.
Instances For
The triple is additive, because each of its three coordinates is.
Equations
- Dc.toNumClassHom = AddMonoidHom.mk' Dc.toNumClass ⋯
Instances For
The alignmentLocus-plane discriminant of the transported triple is the compressed discriminant.
The (s,t) charge of the transported triple is the scalar-twisted
charge. This is the identity that makes the whole (s,t) development
available to any compressed coordinates.
The (s,t) alignmentLocus family of compressed coordinates: the generic (s,t) child
pulled back along the degree-weighted triple.
Equations
Instances For
Twisting the character moves the B-field #
Twisting the character adds to the B-field. This is
exp(-B₀) exp(-B) = exp(-(B₀+B)) read on the central charge, and it is what
lets a slice absorb its transverse direction into the character.
A fixed transverse parameter gives an (s, t) half plane #
The slice point at a fixed transverse parameter, as a function of (s, t).
Equations
- CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point.ofST uu p = { s := p.1, u := uu, t := p.2 }
Instances For
The compressed coordinates a fixed u-slice sees: the G(u)-twisted
character, read at H.
Equations
- T.sliceCoordinates ch uu = (ch.twist S (T.transverse uu)).coordinatesAt S T.H
Instances For
The compressed degree does not see the transverse direction, because
G(u) is orthogonal to H.
The fixed-u slice of a divisorial alignmentLocus family is the (s,t) model.
Reindexing the divisorial family to a fixed transverse parameter gives exactly
the generic (s,t) charge family, pulled back along the degree-weighted triple
of the G(u)-twisted character. Every circle, line, disjointness and nesting
theorem of Walls/Numerical/ therefore applies on that half plane.
The alignmentLocus of two classes on a fixed u-slice is the (s,t) alignmentLocus of their
transported triples.
The circle, on every slice #
A numerical alignmentLocus on a fixed u-slice is cut out by a circle equation.
Maciocia Prop. 2.6; Mizuno--Yoshida Thm 2.1(1).
Centre (-minB/minA, 0) and radius squared (minB² - 2 minA minC)/minA²,
on a fixed u-slice, in cleared form.
The vertical-line case, on a fixed u-slice.
The discriminant on a slice #
The slice discriminant, expanded. The transverse direction contributes
2 H² r (G(u) · ch₁) - H² r² G(u)², so the walls of one class genuinely move
with u.
The bar discriminant at a slice point is t² times the slice
discriminant. The s-dependence cancels exactly, which is why
\bar Δ^B_ω is constant along each vertical line of the half plane.
Bogomolov--Gieseker and a Hodge index discharge the discriminant
hypothesis on every u-slice. This is what the disjointness and nesting
theorems of Walls/Numerical/ need, and until now it was available only on the
rank-one transport.
The same, against the alignmentLocus-plane discriminant the (s,t) theorems consume.