Real divisor realizations of numerical surface data

NumericalRingData stores a rational graded intersection ring, whereas a surface stability condition uses divisor parameters in N^1(X)_ℝ. This file is the bridge between those layers.

A Surface.NumericalRealization sends the codimension-one piece of a numerical intersection ring additively into a real divisor space, respects rational scalars after the inclusion ℚ → ℝ, and identifies multiplication followed by degree with the real intersection form. Given any NumericalVarietyData using that ring, it then constructs the full ChernCharacter; no basis or Picard-rank hypothesis is involved.

The main compatibility theorem identifies the resulting intrinsic divisorial charge at

B = realize(B₀), omega = a * realize(H)

with the existing charge obtained directly from a rational BField B₀ and a Polarization H. Thus the rational ring presentation is a source of concrete children of DivisorialCharge, rather than a competing central-charge API.

structure AlgebraicGeometry.Numerical.Surface.NumericalRealization {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] (S : NumericalRingData 2 A) : Type (max u w)

A realization of rational numerical divisor classes in a real divisor space, preserving the surface intersection form.

The scalar law is stated explicitly instead of asking typeclass inference to choose a ℚ-module structure on D; the intended scalar action is always the one obtained from ℚ → ℝ.

• divisorSpace : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace D

  The real numerical divisor space.

• divisorClass : ↥(S.piece 1) →+ D

  Realization of the rational codimension-one piece.

• map_rat_smul (q : ℚ) (x : ↥(S.piece 1)) : self.divisorClass (q • x) = ↑q • self.divisorClass x

  Compatibility with extension of scalars from ℚ to ℝ.

• intersection_eq (x y : ↥(S.piece 1)) : self.divisorSpace.pair (self.divisorClass x) (self.divisorClass y) = ↑(S.degree (↑x * ↑y))

  Multiplication and degree compute the realized intersection pairing.

def AlgebraicGeometry.Numerical.Surface.NumericalRealization.chOneClassHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) : N →+ ↥(V.ring.piece 1)

The codimension-one Chern-character component as an additive map into its graded piece.

Equations

• AlgebraicGeometry.Numerical.Surface.NumericalRealization.chOneClassHom V = AddMonoidHom.mk' (fun (E : N) => ⟨V.chComp E 1, ⋯⟩) ⋯

noncomputable def AlgebraicGeometry.Numerical.Surface.NumericalRealization.chernCharacter {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) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter N D

The full real Chern character induced by a numerical surface presentation.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.chernCharacter_rank {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) (E : N) : R.chernCharacter.rank E = ↑(V.rank E)

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.chernCharacter_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) (E : N) : R.chernCharacter.chOne E = R.divisorClass ⟨V.chComp E 1, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.chernCharacter_chTwo {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) (E : N) : R.chernCharacter.chTwo E = ↑(V.ring.degree (V.chComp E 2))

def AlgebraicGeometry.Numerical.Surface.NumericalRealization.realizeBField {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) (B : BField V.ring) : D

Realize a rational numerical B-field.

Equations

• R.realizeBField B = R.divisorClass ⟨B.cls, ⋯⟩

def AlgebraicGeometry.Numerical.Surface.NumericalRealization.realizePolarization {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) : D

Realize the divisor class underlying a polarization.

Equations

• R.realizePolarization P = R.divisorClass ⟨P.cls, ⋯⟩

def AlgebraicGeometry.Numerical.Surface.NumericalRealization.parameters {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) (B : BField V.ring) (a : ℝ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D

Parameters obtained from a rational B-field and a real multiple of a realized polarization.

Equations

• R.parameters P B a = { B := R.realizeBField B, omega := a • R.realizePolarization P }

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.twist_chOne_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) (B : BField V.ring) (E : N) : (R.chernCharacter.twist R.divisorSpace (R.realizeBField B)).chOne E = R.divisorClass ⟨chBComp V B E 1, ⋯⟩

Realization commutes with the degree-one part of the B-twisted Chern character.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.twist_chTwo_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) (B : BField V.ring) (E : N) : (R.chernCharacter.twist R.divisorSpace (R.realizeBField B)).chTwo E = ↑(V.ring.degree (chBComp V B E 2))

Realization commutes with the integrated degree-two part of the B-twisted Chern character.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.parameters_omega_square {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) (B : BField V.ring) (a : ℝ) : R.divisorSpace.pair (R.parameters P B a).omega (R.parameters P B a).omega = a ^ 2 * ↑(V.ring.degree (P.cls ^ 2))

The square of a realized, real-scaled polarization is the scalar extension of its rational self-intersection.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.parameters_pair_twist_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) (B : BField V.ring) (a : ℝ) (E : N) : R.divisorSpace.pair (R.parameters P B a).omega ((R.chernCharacter.twist R.divisorSpace (R.realizeBField B)).chOne E) = a * ↑(V.ring.degree (chBComp V B E 1 * P.cls))

Pairing the realized polarization with the realized twisted first Chern class recovers the rational twisted degree.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.centralCharge_eq_ofNumericalDataB {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) (B : BField V.ring) (a : ℝ) (E : N) : (R.chernCharacter.centralCharge R.divisorSpace (R.parameters P B a)) E = ((CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB V P B).centralCharge a) E

The intrinsic real divisorial charge agrees with the existing numerical ring charge whenever B and the polarization come from the rational presentation.