Numerical intersection data for a smooth quadric surface

For a smooth quadric surface Q = P¹ × P¹, the rational numerical intersection ring is

ℚ[f₁,f₂] / (f₁²,f₂²)

with ∫ f₁f₂ = 1. We realize it as dual numbers in f₂ over the dual numbers in f₁. Its product basis has weights 0,1,1,2; this produces an honest NumericalRingData rather than merely a coordinate formula.

The real divisor realization sends c f₁ + d f₂ to (c,d) and recovers the intersection form ((c,d),(c',d')) ↦ c d' + d c' used by the divisorial surface charge. This remains an explicit numerical presentation: it does not identify the carrier with the geometric K_num(Q) or construct the geometric Chern-character map from coherent sheaves.

The rational intersection ring

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Ring : Type

The four-dimensional algebra ℚ[f₁,f₂]/(f₁²,f₂²).

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Ring = DualNumber (DualNumber ℚ)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ : Ring

The first ruling class.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ = ((0, 1), 0, 0)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ : Ring

The second ruling class.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ = ((0, 0), 1, 0)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ : Ring

The point class f₁f₂.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ = ((0, 0), 0, 1)

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ_mul_self : rulingOneQ * rulingOneQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ_sq : rulingOneQ ^ 2 = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ_mul_self : rulingTwoQ * rulingTwoQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ_sq : rulingTwoQ ^ 2 = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ_mul_rulingTwoQ : rulingOneQ * rulingTwoQ = pointQ

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ_mul_rulingOneQ : rulingTwoQ * rulingOneQ = pointQ

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ_mul_pointQ : rulingOneQ * pointQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ_mul_pointQ : rulingTwoQ * pointQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ_mul_rulingOneQ : pointQ * rulingOneQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ_mul_rulingTwoQ : pointQ * rulingTwoQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ_mul_self : pointQ * pointQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ_sq : pointQ ^ 2 = 0

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.coordEquiv : Ring ≃ₗ[ℚ] Fin 4 → ℚ

Coordinates in the ordered basis 1,f₁,f₂,f₁f₂.

This equivalence is explicit because the scalar-module instance on a trivial square-zero extension is not definitionally the product-module instance.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis : Module.Basis (Fin 4) ℚ Ring

The product basis 1,f₁,f₂,f₁f₂.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis = Module.Basis.ofEquivFun AlgebraicGeometry.Numerical.Examples.SmoothQuadric.coordEquiv

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight : Fin 4 → ℕ

Codimension weights on the product basis.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight = ![0, 1, 1, 2]

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis_zero : basis 0 = 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis_one : basis 1 = rulingOneQ

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis_two : basis 2 = rulingTwoQ

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis_three : basis 3 = pointQ

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight_zero : weight 0 = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight_one : weight 1 = 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight_two : weight 2 = 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight_three : weight 3 = 2

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weight_le_two (i : Fin 4) : weight i ≤ 2

Every basis weight is at most the surface dimension.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.basis_mul_mem (p q : Fin 4) : basis p * basis q ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑basis) weight (weight p + weight q)

The multiplicative grading, checked on the four basis vectors.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree : Ring →ₗ[ℚ] ℚ

Integration extracts the coefficient of f₁f₂.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_one : degree 1 = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_rulingOneQ : degree rulingOneQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_rulingTwoQ : degree rulingTwoQ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_pointQ : degree pointQ = 1

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_basis_of_ne (i : Fin 4) (hi : weight i ≠ 2) : degree (basis i) = 0

Integration vanishes on every basis vector outside codimension two.

@[reducible]

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRing : NumericalRingData 2 Ring

The rational numerical intersection ring of the smooth quadric.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_ruling_product : numericalRing.degree (rulingOneQ * rulingTwoQ) = 1

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_mul (x y : Ring) : degree (x * y) = (TrivSqZeroExt.fst x).fst * (TrivSqZeroExt.snd y).snd + (TrivSqZeroExt.fst x).snd * (TrivSqZeroExt.snd y).fst + (TrivSqZeroExt.snd x).fst * (TrivSqZeroExt.fst y).snd + (TrivSqZeroExt.snd x).snd * (TrivSqZeroExt.fst y).fst

Integration of a product in the four coordinates 1,f₁,f₂,f₁f₂.

Numerical Chern and Todd data

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.SmoothQuadric.NumericalClass : Type

Numerical classes in coordinates (rank, f₁ coefficient, f₂ coefficient, ch₂).

Unlike the projective-plane lattice, no half-integral reparametrization is needed: for O(a,b), the top Chern-character coefficient is ab.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.NumericalClass = (ℤ × ℤ × ℤ × ℤ)

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp (E : NumericalClass) : ℕ → Ring

The Chern-character components in the quadric intersection ring.

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp E 0 = (algebraMap ℚ AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Ring) ↑E.1
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp E 2 = ↑E.2.2.2 • AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp E n.succ.succ.succ = 0

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ_mem : rulingOneQ ∈ numericalRing.piece 1

The four basis vectors lie in their stated codimensions.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ_mem : rulingTwoQ ∈ numericalRing.piece 1

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ_mem : pointQ ∈ numericalRing.piece 2

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp_mem (E : NumericalClass) (i : ℕ) : chComp E i ∈ numericalRing.piece i

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chComp_add (E F : NumericalClass) (i : ℕ) : chComp (E + F) i = chComp E i + chComp F i

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.ch_sum (E : NumericalClass) : ∑ i ∈ Finset.range (2 + 1), chComp E i = ((↑E.1, ↑E.2.1), ↑E.2.2.1, ↑E.2.2.2)

The total Chern character in the explicit four-coordinate carrier.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp : ℕ → Ring

The Todd class of P¹ × P¹ is 1 + (f₁+f₂) + f₁f₂.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp 0 = 1
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp 1 = AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ + AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp 2 = AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pointQ
• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp n.succ.succ.succ = 0

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.toddComp_mem (i : ℕ) : toddComp i ∈ numericalRing.piece i

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.todd_sum : ∑ i ∈ Finset.range (2 + 1), toddComp i = ((1, 1), 1, 1)

The total Todd class in the explicit four-coordinate carrier.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chi : NumericalClass →+ ℤ

Euler characteristic in the chosen integral coordinates.

Equations

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

@[reducible]

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalVariety : NumericalVarietyData 2 Ring NumericalClass

The rational numerical presentation of a smooth quadric surface.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalVariety_satisfiesHRR : numericalVariety.SatisfiesHRR

The selected presentation satisfies Hirzebruch--Riemann--Roch.

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segreQ : Ring

The Segre polarization f₁+f₂ in the rational intersection ring.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segreQ = AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOneQ + AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwoQ

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segreQ_eq : segreQ = ((0, 1), 1, 0)

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segreQ_mem : segreQ ∈ numericalRing.piece 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_segreQ_sq : numericalRing.degree (segreQ ^ 2) = 2

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.polarizationClass (h₁ h₂ : ℚ) : Ring

A rational divisor class in ruling coordinates.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.polarizationClass_mem (h₁ h₂ : ℚ) : polarizationClass h₁ h₂ ∈ numericalRing.piece 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.degree_polarizationClass_sq (h₁ h₂ : ℚ) : numericalRing.degree (polarizationClass h₁ h₂ ^ 2) = 2 * h₁ * h₂

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.polarization (h₁ h₂ : ℚ) (hh₁ : 0 < h₁) (hh₂ : 0 < h₂) : Polarization numericalVariety.ring

An ample rational polarization h₁f₁+h₂f₂ with both ruling coefficients positive.

Equations

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

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segrePolarization : Polarization numericalVariety.ring

The Segre class as a rational polarization.

Equations

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

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.bField (b₁ b₂ : ℚ) : BField numericalVariety.ring

An arbitrary rational B = b₁f₁+b₂f₂.

Equations

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

Real divisor realization

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Divisor : Type

Real numerical divisor classes, in the ruling basis.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.Divisor = (ℝ × ℝ)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOne : Divisor

The first real ruling class.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOne = (1, 0)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwo : Divisor

The second real ruling class.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwo = (0, 1)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segre : Divisor

The real Segre class f₁+f₂.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.segre = (1, 1)

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.intersectionForm : LinearMap.BilinForm ℝ Divisor

The intersection form in ruling coordinates.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.intersectionForm_apply (x y : Divisor) : (intersectionForm x) y = x.1 * y.2 + x.2 * y.1

def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorSpace : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace Divisor

The rank-two real divisor space of the smooth quadric.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOne_sq : divisorSpace.pair rulingOne rulingOne = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingTwo_sq : divisorSpace.pair rulingTwo rulingTwo = 0

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.rulingOne_pair_rulingTwo : divisorSpace.pair rulingOne rulingTwo = 1

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.weightOneBasis : ⇑basis '' weight ⁻¹' {1} = {rulingOneQ, rulingTwoQ}

The weight-one basis vectors are precisely the two rational rulings.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.pieceOne_eq_span_rulings : numericalRing.piece 1 = Submodule.span ℚ {rulingOneQ, rulingTwoQ}

The rational divisor piece is the two-dimensional span of the rulings.

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorClass : ↥(numericalRing.piece 1) →+ Divisor

Extend a rational divisor class to real ruling coordinates.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorClass_map_rat_smul (q : ℚ) (x : ↥(numericalRing.piece 1)) : divisorClass (q • x) = ↑q • divisorClass x

The divisor realization commutes with extension of scalars ℚ → ℝ.

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.divisorClass_intersection (x y : ↥(numericalRing.piece 1)) : divisorSpace.pair (divisorClass x) (divisorClass y) = ↑(numericalRing.degree (↑x * ↑y))

Multiplication in the rational ring realizes to the ruling intersection form.

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRealization : Surface.NumericalRealization numericalVariety.ring

The rational numerical ring realized in N¹(Q)_ℝ.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chernCharacter : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter NumericalClass Divisor

The full real Chern character induced from the rational numerical presentation.

Equations

• AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chernCharacter = AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRealization.chernCharacter

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chernCharacter_rank (E : NumericalClass) : chernCharacter.rank E = ↑E.1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chernCharacter_chOne (E : NumericalClass) : chernCharacter.chOne E = (↑E.2.1, ↑E.2.2.1)

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.chernCharacter_chTwo (E : NumericalClass) : chernCharacter.chTwo E = ↑E.2.2.2

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRealization_segre : numericalRealization.realizePolarization segrePolarization = segre

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRealization_polarization (h₁ h₂ : ℚ) (hh₁ : 0 < h₁) (hh₂ : 0 < h₂) : numericalRealization.realizePolarization (polarization h₁ h₂ hh₁ hh₂) = (↑h₁, ↑h₂)

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.SmoothQuadric.numericalRealization_bField (b₁ b₂ : ℚ) : numericalRealization.realizeBField (bField b₁ b₂) = (↑b₁, ↑b₂)