The projective-plane child of the divisorial surface charge

This file instantiates the intrinsic divisorial surface construction for ℙ². Its divisor space is one-dimensional, with the hyperplane class H normalized by H² = 1. Two class carriers carry a full ChernCharacter: a placeholder integral triple (r, c, v) and the existing SurfaceNum presentation. Their comparison is made before choosing B and omega.

What is, and is not, compared here

The two carriers have identical coordinates: on both, ch₂ = c/2 + v, and the comparison map p2ProjectiveToSurface is the identity on coordinates. The theorem p2ProjectiveCharge_eq_surfaceCharge is therefore an instance of ChernCharacter.Pullback.centralCharge_eq applied to an identity witness; it is not a comparison between Li's image lattice Λ_ι and the surface lattice, because nothing in this file is Λ_ι or v_ι. The mathematical content is the identity -∫ exp(-(b + i a) H) ch = Z_{aH, bH}, which is ChargeCoordinates.centralCharge_twistByScalar_apply and holds on every polarised surface; p2ProjectiveCharge_apply records it in the (r, c, v) coordinates. The only ℙ²-specific input is H² = 1, which makes the compressed degree H · ch₁ equal to the full first Chern class.

The exponential presentation is the projective-space charge of the projective-family construction for the identity embedding ℙ² ⊂ ℙ², the one case in which no Todd correction appears (arXiv:2607.28411v1, (5.5) and Remark 6.3). For any other embedding the pulled-back charge is not of this form until the GRR/Todd term has been computed.

The older scalar ChargeCoordinates objects are derived compatibility views. Thus the projective-plane charge is a child of the same parent as the smooth-quadric charge, rather than a parent or a separate charge polynomial.

The adapter is only arithmetic. It does not claim that either carrier is K₀(ℙ²) or Λ_ι, does not compare stability conditions, hearts, or slicings, and does not provide the geometric family map or the C1/C2 properties needed by the eventual stability comparison.

The projective-plane divisor space

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.P2Divisor : Type

Real numerical divisor classes on ℙ², represented in the hyperplane basis.

Equations

• AlgebraicGeometry.Numerical.Examples.P2Divisor = ℝ

def AlgebraicGeometry.Numerical.Examples.p2IntersectionForm : LinearMap.BilinForm ℝ P2Divisor

The intersection form in the normalized hyperplane basis.

Equations

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

def AlgebraicGeometry.Numerical.Examples.p2DivisorSpace : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace P2Divisor

The rank-one numerical divisor space of ℙ².

Equations

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

def AlgebraicGeometry.Numerical.Examples.p2Hyperplane : P2Divisor

The hyperplane generator in the one-dimensional divisor space.

Equations

• AlgebraicGeometry.Numerical.Examples.p2Hyperplane = 1

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2Hyperplane_square : p2DivisorSpace.pair p2Hyperplane p2Hyperplane = 1

The two full Chern-character presentations

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.P2ProjectiveCoordinates : Type

A placeholder integral (r, c, v) carrier for the exponential presentation of the charge.

It has the same coordinates as SurfaceNum (ch₂ = c/2 + v on both) and is a separate Lean type only so that the adapter below carries an explicit source-to-target map, where a geometric class map can later be substituted. It is not Li's image lattice Λ_ι and carries no information about K₀(ℙ²).

Equations

• AlgebraicGeometry.Numerical.Examples.P2ProjectiveCoordinates = (ℤ × ℤ × ℤ)

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ProjectiveChernCharacter : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter P2ProjectiveCoordinates P2Divisor

The full Chern character on the explicit projective-family coordinates.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ProjectiveChargeCoordinates : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates P2ProjectiveCoordinates

The old scalar-coordinate view, derived from the full character at H.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveChargeCoordinates_rank (E : P2ProjectiveCoordinates) : p2ProjectiveChargeCoordinates.rank E = ↑E.1

The source rank coordinate is the first projective triple entry.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveChargeCoordinates_degree (E : P2ProjectiveCoordinates) : p2ProjectiveChargeCoordinates.degree E = ↑E.2.1

The source degree coordinate is the second projective triple entry.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveChargeCoordinates_chTwo (E : P2ProjectiveCoordinates) : p2ProjectiveChargeCoordinates.chTwo E = ↑E.2.1 / 2 + ↑E.2.2

The source ch₂ coordinate is c/2 + v.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveChargeCoordinates_hyperplaneSquare : p2ProjectiveChargeCoordinates.hyperplaneSquare = 1

The projective-plane source uses the normalization H² = 1.

noncomputable def AlgebraicGeometry.Numerical.Examples.p2Polarization : Polarization p2NumericalVariety.ring

The hyperplane class as the polarisation used by the ℙ² surface model.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2BField (β : ℚ) : BField p2NumericalVariety.ring

The projective-plane B-field B = βH in the rational numerical ring.

Every rational numerical divisor class on this rank-one model has this form. The real scalar API below extends the same coordinate formula to real b.

Equations

• AlgebraicGeometry.Numerical.Examples.p2BField β = AlgebraicGeometry.Numerical.BField.along AlgebraicGeometry.Numerical.Examples.p2Polarization β

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2BField_cls (β : ℚ) : (p2BField β).cls = (algebraMap ℚ SurfaceRing) β * H

The named projective-plane B-field evaluates to βH.

Real realization of the rational divisor piece

def AlgebraicGeometry.Numerical.Examples.p2DivisorIndex : Fin surfacePB.dim

The unique basis index of codimension one in the rank-one surface ring.

Equations

• AlgebraicGeometry.Numerical.Examples.p2DivisorIndex = ⟨1, AlgebraicGeometry.Numerical.Examples.p2DivisorIndex._proof_1⟩

theorem AlgebraicGeometry.Numerical.Examples.surfaceWeightOneBasis : ⇑surfacePB.basis '' surfaceW ⁻¹' {1} = {H}

The weight-one basis vectors are exactly the singleton H.

theorem AlgebraicGeometry.Numerical.Examples.surfacePieceOne_eq_span_H : p2NumericalVariety.ring.piece 1 = ℚ ∙ H

The codimension-one graded piece of the projective-plane ring is the one-dimensional span of H.

noncomputable def AlgebraicGeometry.Numerical.Examples.p2DivisorClass : ↥(p2NumericalVariety.ring.piece 1) →+ P2Divisor

Realize a rational divisor class by its coefficient in the hyperplane basis, computed invariantly as ∫xH using H² = 1.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.p2DivisorClass_map_rat_smul (q : ℚ) (x : ↥(p2NumericalVariety.ring.piece 1)) : p2DivisorClass (q • x) = ↑q • p2DivisorClass x

The hyperplane-coefficient realization respects rational scalar extension.

theorem AlgebraicGeometry.Numerical.Examples.p2DivisorClass_intersection (x y : ↥(p2NumericalVariety.ring.piece 1)) : p2DivisorSpace.pair (p2DivisorClass x) (p2DivisorClass y) = ↑(p2NumericalVariety.ring.degree (↑x * ↑y))

On the codimension-one piece, multiplication followed by degree is the ordinary product of realized hyperplane coefficients.

noncomputable def AlgebraicGeometry.Numerical.Examples.p2NumericalRealization : Surface.NumericalRealization p2NumericalVariety.ring

The projective-plane numerical ring realized in N¹(P²)_ℝ.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2NumericalRealization_divisorSpace : p2NumericalRealization.divisorSpace = p2DivisorSpace

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2NumericalRealization_polarization : p2NumericalRealization.realizePolarization p2Polarization = p2Hyperplane

The rational hyperplane realizes to the chosen real hyperplane.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2NumericalRealization_BField (β : ℚ) : p2NumericalRealization.realizeBField (p2BField β) = ↑β • p2Hyperplane

The rational field βH realizes to the real divisor βH.

noncomputable def AlgebraicGeometry.Numerical.Examples.p2SurfaceChargeCoordinates : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates SurfaceNum

The surface-side charge coordinates induced by the numerical presentation.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2SurfaceChernCharacter : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter SurfaceNum P2Divisor

The full Chern character on the existing surface numerical presentation.

Because N¹(ℙ²)_ℝ = ℝH and H² = 1, the old H-degree is exactly the coefficient of the full first Chern class.

Equations

• AlgebraicGeometry.Numerical.Examples.p2SurfaceChernCharacter = AlgebraicGeometry.Numerical.Examples.p2NumericalRealization.chernCharacter

The explicit numerical comparison map

def AlgebraicGeometry.Numerical.Examples.p2ProjectiveToSurface : P2ProjectiveCoordinates →+ SurfaceNum

The source-to-target additive map sending (r, c, v) to ![r, c, v].

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChargeCoordinates_rank (E : SurfaceNum) : p2SurfaceChargeCoordinates.rank E = ↑(E 0)

The target rank coordinate is the first SurfaceNum entry.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChargeCoordinates_degree (E : SurfaceNum) : p2SurfaceChargeCoordinates.degree E = ↑(E 1)

The target polarised degree is the second SurfaceNum entry.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChargeCoordinates_chTwo (E : SurfaceNum) : p2SurfaceChargeCoordinates.chTwo E = ↑(E 1) / 2 + ↑(E 2)

The target integrated ch₂ is the projective c/2 + v coordinate.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChargeCoordinates_hyperplaneSquare : p2SurfaceChargeCoordinates.hyperplaneSquare = 1

The chosen target polarisation has square one.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChernCharacter_rank (E : SurfaceNum) : p2SurfaceChernCharacter.rank E = ↑(E 0)

The realized surface rank is the first numerical coordinate.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChernCharacter_chOne (E : SurfaceNum) : p2SurfaceChernCharacter.chOne E = ↑(E 1)

The realized full first Chern class is its hyperplane coefficient.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceChernCharacter_chTwo (E : SurfaceNum) : p2SurfaceChernCharacter.chTwo E = ↑(E 1) / 2 + ↑(E 2)

The realized integrated second Chern character is unchanged.

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ChernCharacterPullback : p2ProjectiveChernCharacter.Pullback p2SurfaceChernCharacter

The two presentations preserve the full Chern character, before any choice of B-field or ample class. Consequently this one witness compares all projective-plane divisorial charges.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2SurfaceCoordinatesPullback : (p2SurfaceChernCharacter.coordinatesAt p2DivisorSpace p2Hyperplane).Pullback p2SurfaceChargeCoordinates

The coordinates derived from the full surface character agree with the legacy numerical coordinates. This bridge exists only because H² = 1 on the chosen rank-one basis.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ChargePullback : p2ProjectiveChargeCoordinates.Pullback p2SurfaceChargeCoordinates

The full-character comparison induces the legacy scalar-coordinate comparison at the projective hyperplane.

Equations

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

The two presentations of the same charge

def AlgebraicGeometry.Numerical.Examples.p2Parameters (a b : ℝ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters P2Divisor

The projective-plane rank-one family B = bH, omega = aH, obtained as a specialization of the parent parameter space.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge (a b : ℝ) : P2ProjectiveCoordinates →+ ℂ

The divisorial parent charge on the placeholder (r, c, v) carrier at B = bH, omega = aH. Its expansion p2ProjectiveCharge_apply is the projective-space exponential -∫ exp(-(b + i a) H) ch; the carrier is not Li's image lattice.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2SurfaceCharge (a b : ℝ) : SurfaceNum →+ ℂ

The same parent charge on the existing SurfaceNum presentation.

Equations

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

The inherited rank-one wall slice

def AlgebraicGeometry.Numerical.Examples.p2WallSlice : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice p2DivisorSpace (Fin 0 → ℝ)

The projective-plane wall slice has no transverse directions.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Examples.p2ProjectiveWallFamily : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point (Fin 0 → ℝ)) P2ProjectiveCoordinates

The projective-coordinate charge as a child of the generic wall-family and orthogonal-slice layers.

Equations

• AlgebraicGeometry.Numerical.Examples.p2ProjectiveWallFamily = AlgebraicGeometry.Numerical.Examples.p2WallSlice.chargeFamily AlgebraicGeometry.Numerical.Examples.p2ProjectiveChernCharacter

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveWallFamily_charge (a b : ℝ) (E : P2ProjectiveCoordinates) : (p2ProjectiveWallFamily.charge (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point.rankOne b a)) E = (p2ProjectiveCharge a b) E

Evaluating the inherited rank-one family recovers the existing projective-plane charge.

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge_zero (a b : ℝ) : (p2ProjectiveCharge a b) 0 = 0

The projective charge respects the additive zero class.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceCharge_zero (a b : ℝ) : (p2SurfaceCharge a b) 0 = 0

The surface charge respects the additive zero class.

theorem AlgebraicGeometry.Numerical.Examples.p2SurfaceCharge_eq_BFieldCharge (a : ℝ) (β : ℚ) (E : SurfaceNum) : (p2SurfaceCharge a ↑β) E = ((CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB p2NumericalVariety p2Polarization (p2BField β)).centralCharge a) E

For rational β, the real scalar presentation is exactly the charge built from the general twisted Chern character at B = βH.

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge_eq_surfaceCharge (a b : ℝ) (E : P2ProjectiveCoordinates) : (p2ProjectiveCharge a b) E = (p2SurfaceCharge a b) (p2ProjectiveToSurface E)

The two presentations of the parent charge agree under the identity parameter map and the coordinate map p2ProjectiveToSurface.

This is ChernCharacter.Pullback.centralCharge_eq for the identity-on- coordinates witness p2ChernCharacterPullback; it compares two Lean carriers with the same coordinates, not two different lattices. See the module docstring for what this does and does not establish.

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge_apply (a b : ℝ) (E : P2ProjectiveCoordinates) : (p2ProjectiveCharge a b) E = -↑(↑E.2.1 / 2 + ↑E.2.2) + (↑b + ↑a * Complex.I) * ↑↑E.2.1 - (↑b + ↑a * Complex.I) ^ 2 * ↑(↑E.1 / 2)

The projective-space exponential -∫ exp(-(b + i a) H) ch in the (r, c, v) coordinates: the surface charge at B = bH, omega = aH equals the exponential presentation with H² = 1.

Coordinate formulas

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge_re (a b : ℝ) (E : P2ProjectiveCoordinates) : ((p2ProjectiveCharge a b) E).re = -(↑E.2.1 / 2 + ↑E.2.2) + b * ↑E.2.1 + (a ^ 2 - b ^ 2) * (↑E.1 / 2)

The real part of the projective-plane charge in (r, c, v) coordinates.

theorem AlgebraicGeometry.Numerical.Examples.p2ProjectiveCharge_im (a b : ℝ) (E : P2ProjectiveCoordinates) : ((p2ProjectiveCharge a b) E).im = a * ↑E.2.1 - 2 * a * b * (↑E.1 / 2)

The imaginary part of the projective-plane charge in (r, c, v) coordinates.