The divisorial central charge on a smooth quadric surface

Over an algebraically closed field, the smooth quadric surface is Q = P^1 x P^1. Its real numerical divisor space has basis given by the two rulings f₁, f₂, with

f₁^2 = f₂^2 = 0, f₁.f₂ = 1.

This is the first example in which a scalar field B = beta H is not the intrinsic parameter. We model

H = h₁ f₁ + h₂ f₂, B = b₁ f₁ + b₂ f₂

independently and recover the explicit rank-two formula. The ample cone is recorded separately as h₁ > 0 and h₂ > 0, while the arithmetic central charge itself remains defined for every pair of real classes.

The numerical carrier uses coordinates (r, c, d, v) for ch(E) = (r, c f₁ + d f₂, v). Its real Chern character is induced from the rational graded ring through Surface.NumericalRealization, so this charge is a child of the general divisorial construction rather than an independent coordinate polynomial.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.parameters (h₁ h₂ b₁ b₂ : ℝ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters Divisor

Independent real parameters in the ruling basis.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.parameters h₁ h₂ b₁ b₂ = { B := (b₁, b₂), omega := (h₁, h₂) }

The arbitrary real scalar-extension presentation

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.scalarExtendedDivisor (x y : ℝ) : Surface.RealDivisorClass numericalRing

A real divisor class in the rational ruling basis, regarded as an element of ℝ ⊗[ℚ] A¹(Q)_ℚ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.realize_scalarExtendedDivisor (x y : ℝ) : numericalRealization.extendDivisorClass (scalarExtendedDivisor x y) = (x, y)

The scalar-extended ruling coordinates realize to the corresponding arbitrary real class in N¹(Q)_ℝ.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.extendDivisorClass_surjective : Function.Surjective ⇑numericalRealization.extendDivisorClass

The scalar-extension realization reaches every real divisor class on the smooth quadric.

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.scalarExtendedParameters (h₁ h₂ b₁ b₂ : ℝ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters (Surface.RealDivisorClass numericalRing)

Independent real B and omega in the scalar extension of the quadric's rational numerical ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.realize_scalarExtendedParameters (h₁ h₂ b₁ b₂ : ℝ) : numericalRealization.realizeParameters (scalarExtendedParameters h₁ h₂ b₁ b₂) = parameters h₁ h₂ b₁ b₂

Realizing scalar-extended parameters recovers the intrinsic ruling coordinates.

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.charge (h₁ h₂ b₁ b₂ : ℝ) : NumericalClass →+ ℂ

The smooth-quadric child of the intrinsic divisorial central charge.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.charge_eq_scalarExtension (h₁ h₂ b₁ b₂ : ℝ) (E : NumericalClass) : (charge h₁ h₂ b₁ b₂) E = (Surface.ScalarExtension.chernCharacter.centralCharge (Surface.RealDivisorClass.divisorSpace numericalRing) (scalarExtendedParameters h₁ h₂ b₁ b₂)) E

The coordinate charge is exactly the canonical scalar-extension charge for every real pair B = (b₁,b₂) and omega = (h₁,h₂). Unlike the rational compatibility theorem below, this statement loses no real divisor classes.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.ampleCone : Set Divisor

The ample cone of the smooth quadric in ruling coordinates.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.ampleCone = {H : AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Divisor | 0 < H.1 ∧ 0 < H.2}

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorialParameters (h₁ h₂ b₁ b₂ : ℝ) (hh₁ : 0 < h₁) (hh₂ : 0 < h₂) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorialParameters ampleCone

Bundle the geometric ampleness side condition without changing the charge arithmetic.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorialParameters h₁ h₂ b₁ b₂ hh₁ hh₂ = { B := (b₁, b₂), omega := (h₁, h₂), omega_ample := ⋯ }

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.omega_square (h₁ h₂ : ℝ) : divisorSpace.pair (h₁, h₂) (h₁, h₂) = 2 * h₁ * h₂

The polarization square is 2 h₁ h₂.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.omega_square_pos {h₁ h₂ : ℝ} (hh₁ : 0 < h₁) (hh₂ : 0 < h₂) : 0 < divisorSpace.pair (h₁, h₂) (h₁, h₂)

An ample class on the smooth quadric has positive square. This is a derived fact in the example, not the definition of ampleness in the core API.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.centralCharge_apply (h₁ h₂ b₁ b₂ : ℝ) (r c d v : ℤ) : (charge h₁ h₂ b₁ b₂) (r, c, d, v) = ↑(-↑v + b₁ * ↑d + b₂ * ↑c + (h₁ * h₂ - b₁ * b₂) * ↑r) + Complex.I * ↑(h₁ * ↑d + h₂ * ↑c - (h₁ * b₂ + h₂ * b₁) * ↑r)

Explicit central charge for a smooth quadric in the ruling basis.

For ch(E) = (r, c f₁ + d f₂, v), the real and imaginary parts are

-v + b₁d + b₂c + (h₁h₂-b₁b₂)r, h₁d + h₂c - (h₁b₂+h₂b₁)r.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.charge_eq_numericalBField (a : ℝ) (h₁ h₂ b₁ b₂ : ℚ) (hh₁ : 0 < h₁) (hh₂ : 0 < h₂) (E : NumericalClass) : (charge (a * ↑h₁) (a * ↑h₂) ↑b₁ ↑b₂) E = ((CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB numericalVariety (polarization h₁ h₂ hh₁ hh₂) (bField b₁ b₂)).centralCharge a) E

The intrinsic real charge agrees with the generic numerical-ring charge for arbitrary rational ample polarization and arbitrary rational B-field.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.antiDiagonal (u : ℝ) : Divisor

The direction f₁-f₂, orthogonal to the Segre polarization.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.antiDiagonal u = (u, -u)

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segre_pair_antiDiagonal (u : ℝ) : divisorSpace.pair segre (antiDiagonal u) = 0

The inherited orthogonal wall slice

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.antiDiagonalMap : ℝ →ₗ[ℝ] Divisor

Linear parameterization of the direction transverse to the Segre class.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.wallSlice : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice divisorSpace ℝ

The full rank-two wall slice of the quadric, as a child of the basis-free orthogonal-slice construction.

Equations

• One or more equations did not get rendered due to their size.

The certificates of the slice

Walls/Divisorial/Slice.lean attaches IsHodge and IsGeometric to an orthogonal slice, and wallSlice carried neither. Both hold here, and the pieces were already in the file: the Segre class has positive square, the anti-diagonal direction has negative square, and ampleCone is exactly the set IsGeometric wants.

On a hyperbolic form the first condition is not automatic. ω² = 2h₁h₂ is negative on half the plane and zero on the two rulings, which are isotropic, so H_square_pos genuinely selects the positive cone. That is the difference from the rank-one slice, where every nonzero class has positive square, and it makes the quadric the first slice whose Hodge certificate is neither vacuous nor automatic.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segre_square : divisorSpace.pair segre segre = 2

∫(f₁+f₂)² = 2, so the Segre class has positive square.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.antiDiagonal_square (u : ℝ) : divisorSpace.pair (antiDiagonal u) (antiDiagonal u) = -2 * u ^ 2

The anti-diagonal direction has square -2u²: negative for every nonzero parameter. The ruling classes themselves are isotropic, which is why this needs the anti-diagonal and not an arbitrary transverse direction.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.wallSlice_isHodge : wallSlice.IsHodge

The quadric's wall slice is Hodge.

Not vacuous, unlike the rank-one slice: the transverse space is a line and the second clause has to be checked on it.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segre_mem_ampleCone : segre ∈ ampleCone

The Segre class is ample.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.wallSlice_isGeometric : wallSlice.IsGeometric ampleCone

The quadric's wall slice is geometric.

ampleCone and the slice were both already here; nothing had put them together, so IsGeometric had no witness on this surface.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.not_isHodge_rulingOne (T : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice divisorSpace ℝ) (hH : T.H = rulingOne) : ¬T.IsHodge

The Hodge certificate fails off the positive cone, which is what makes the hyperbolic case different from the definite one.

A ruling class is isotropic, so it cannot be the distinguished direction of any Hodge slice. On a rank-one surface no such class exists.

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.wallChargeFamily : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point ℝ) NumericalClass

The generic wall family specialized to the smooth quadric.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.wallChargeFamily_charge (s u t : ℝ) (E : NumericalClass) : (wallChargeFamily.charge { s := s, u := u, t := t }) E = (charge t t (s + u) (s - u)) E

Evaluating the inherited wall family gives the existing arbitrary-real quadric charge in ruling coordinates.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.antiDiagonal_not_rankOne {u : ℝ} (hu : u ≠ 0) : ¬∃ (beta : ℝ), antiDiagonal u = beta • segre

A nonzero anti-diagonal B-field cannot be represented as beta H for the Segre polarization. This is the concrete information lost by a scalar-only B parameter on a rank-two surface.