Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Stability.DivisorialWallTransport

The (s,t) transport is the rank-one slice of the divisorial family #

WallTransport.lean pulls the three-coordinate (s,t) charge family back to a polarised numerical surface through the degree-weighted toNumClassHom. DivisorialWallSlice.lean builds the arbitrary-(B,ω) charge family of a real divisor space from a full ChernCharacter. Until this file, those two descendants of Wall.ChargeFamily had no theorem connecting them: the hierarchy was a forest with two formula owners, reZ/imZ on one side and ChernCharacter.centralCharge on the other.

For any NumericalRealization of the surface's rational intersection ring in a real divisor space, the two families agree exactly: the compressed (s,t) family is the reindexing of the intrinsic divisorial family along the rank-one slice B = sH, ω = tH, where H is the realized polarisation. Consequently every rank-one child (the K3 model included) reaches both the circle, line, disjointness, and nesting theorems of the (s,t) polynomial and the arbitrary-(B,ω) divisorial layer, and the wall loci of the two presentations coincide pointwise.

Nothing here is geometric: the identity is a match of two arithmetic presentations of -∫ ch₂^B + (ω²/2) ch₀ + i ω·ch₁^B.

source
def AlgebraicGeometry.Numerical.Surface.NumericalRealization.rankOneParameters {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) :
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D

The rank-one slice parameters B = sH, ω = tH of a realized polarisation, indexed by the (s,t) plane of WallTransport.lean.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.rankOneParameters_B {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) :
    (R.rankOneParameters P p).B = p.1 • R.realizePolarization P
    source
    @[simp]
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.rankOneParameters_omega {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) :
    (R.rankOneParameters P p).omega = p.2 • R.realizePolarization P
    source
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.pair_realizePolarization_chOne {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (E : N) :
    R.divisorSpace.pair (R.realizePolarization P) (R.chernCharacter.chOne E) = ↑(degH V P E)

    The realized polarisation pairs with the realized first Chern class to the rational H-degree.

    source
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.pair_realizePolarization_self {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) :
    R.divisorSpace.pair (R.realizePolarization P) (R.realizePolarization P) = ↑(V.ring.degree (P.cls ^ 2))

    The realized polarisation has the rational polarisation square.

    source
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.wallChargeFamily_charge_eq_centralCharge {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) (E : N) :
    ((wallChargeFamily V P).charge p) E = (R.chernCharacter.centralCharge R.divisorSpace (R.rankOneParameters P p)) E

    The two branches of the wall hierarchy agree. The degree-weighted (s,t) charge of WallTransport.lean is the intrinsic divisorial charge at B = sH, ω = tH.

    source
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.wallChargeFamily_eq_rankOne_reindex {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) :
    wallChargeFamily V P = (R.chernCharacter.fullChargeFamily R.divisorSpace).reindex (R.rankOneParameters P)

    The compressed (s,t) family is literally the reindexing of the intrinsic divisorial family along the rank-one slice.

    source
    theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.wallChargeFamily_alignmentLocus_eq {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (v w : N) :
    (wallChargeFamily V P).alignmentLocus v w = R.rankOneParameters P ⁻¹' (R.chernCharacter.fullChargeFamily R.divisorSpace).alignmentLocus v w

    The (s,t) wall of two classes is the rank-one slice of their divisorial wall.