Scalar extension for divisorial surface charges

The numerical intersection ring is naturally defined over ℚ, while the B-field and ample class of a surface stability condition are arbitrary real divisor classes. This file makes the passage between those two coefficient fields explicit.

For a numerical surface ring S, its canonical real divisor space is

RealDivisorClass S = ℝ ⊗[ℚ] S.piece 1.

The rational intersection product extends to this tensor product by base change. Every Surface.NumericalRealization S D then extends uniquely to an ℝ-linear map from RealDivisorClass S to the concrete divisor space D, and that map preserves the intersection form. Consequently arbitrary real B, omega : RealDivisorClass S may be used at the ring-presentation level, not merely rational classes or real multiples of one polarization.

The final compatibility theorem says that the intrinsic central charge is unchanged when all divisor data are transported to any concrete realization. No basis, Picard-rank hypothesis, or choice of generators occurs here.

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Surface.RationalDivisorClass {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : Submodule ℚ A

The rational codimension-one part of a numerical surface ring.

Equations

• AlgebraicGeometry.Numerical.Surface.RationalDivisorClass S = S.piece 1

def AlgebraicGeometry.Numerical.Surface.RationalDivisorClass.intersection {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : LinearMap.BilinForm ℚ ↥(RationalDivisorClass S)

The rational intersection pairing on the codimension-one piece of a numerical surface ring.

Equations

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

theorem AlgebraicGeometry.Numerical.Surface.RationalDivisorClass.intersection_symm {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : (intersection S).IsSymm

The rational divisor intersection pairing is symmetric.

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Surface.RealDivisorClass {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : Type u

The canonical real scalar extension of the rational codimension-one piece. This is the presentation-level model of N¹(X)_ℝ.

Equations

• AlgebraicGeometry.Numerical.Surface.RealDivisorClass S = TensorProduct ℚ ℝ ↥(AlgebraicGeometry.Numerical.Surface.RationalDivisorClass S)

noncomputable def AlgebraicGeometry.Numerical.Surface.RealDivisorClass.ofRational {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) (x : ↥(S.piece 1)) : RealDivisorClass S

Include a rational divisor class into its real scalar extension.

Equations

• AlgebraicGeometry.Numerical.Surface.RealDivisorClass.ofRational S x = 1 ⊗ₜ[ℚ] x

noncomputable def AlgebraicGeometry.Numerical.Surface.RealDivisorClass.intersection {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : LinearMap.BilinForm ℝ (RealDivisorClass S)

The real intersection form obtained by scalar extension from ℚ.

Equations

• AlgebraicGeometry.Numerical.Surface.RealDivisorClass.intersection S = LinearMap.BilinForm.baseChange ℝ (AlgebraicGeometry.Numerical.Surface.RationalDivisorClass.intersection S)

noncomputable def AlgebraicGeometry.Numerical.Surface.RealDivisorClass.divisorSpace {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace (RealDivisorClass S)

The canonical real divisor space attached to a rational numerical surface ring.

Equations

• AlgebraicGeometry.Numerical.Surface.RealDivisorClass.divisorSpace S = { intersection := AlgebraicGeometry.Numerical.Surface.RealDivisorClass.intersection S, intersection_symm := ⋯ }

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.RealDivisorClass.pair_tmul {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) (a b : ℝ) (x y : ↥(S.piece 1)) : (divisorSpace S).pair (a ⊗ₜ[ℚ] x) (b ⊗ₜ[ℚ] y) = ↑(S.degree (↑x * ↑y)) * (a * b)

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.RealDivisorClass.pair_ofRational {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) (x y : ↥(S.piece 1)) : (divisorSpace S).pair (ofRational S x) (ofRational S y) = ↑(S.degree (↑x * ↑y))

noncomputable def AlgebraicGeometry.Numerical.Surface.NumericalRealization.extendDivisorClass {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) : RealDivisorClass S →ₗ[ℝ] D

Extend a rational divisor realization uniquely to the real scalar extension.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.extendDivisorClass_tmul {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) (a : ℝ) (x : ↥(S.piece 1)) : R.extendDivisorClass (a ⊗ₜ[ℚ] x) = a • R.divisorClass x

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.extendDivisorClass_ofRational {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) (x : ↥(S.piece 1)) : R.extendDivisorClass (RealDivisorClass.ofRational S x) = R.divisorClass x

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.extendDivisorClass_unique {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) (f : RealDivisorClass S →ₗ[ℝ] D) (hf : ∀ (x : ↥(S.piece 1)), f (RealDivisorClass.ofRational S x) = R.divisorClass x) : f = R.extendDivisorClass

extendDivisorClass is the unique real-linear extension of the rational divisor realization.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.pair_extendDivisorClass {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) (x y : RealDivisorClass S) : R.divisorSpace.pair (R.extendDivisorClass x) (R.extendDivisorClass y) = (RealDivisorClass.divisorSpace S).pair x y

Scalar extension of a numerical realization preserves the complete real intersection form, not only its values on rational classes.

noncomputable def AlgebraicGeometry.Numerical.Surface.NumericalRealization.realizeParameters {A : Type u} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup D] [Module ℝ D] {S : NumericalRingData 2 A} (R : NumericalRealization S) (P : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters (RealDivisorClass S)) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D

Transport arbitrary real B and omega from the scalar-extended ring presentation to a concrete divisor realization.

Equations

• R.realizeParameters P = { B := R.extendDivisorClass P.B, omega := R.extendDivisorClass P.omega }

noncomputable def AlgebraicGeometry.Numerical.Surface.scalarExtensionRealization {A : Type u} [CommRing A] [Algebra ℚ A] (S : NumericalRingData 2 A) : NumericalRealization S

The rational ring has a canonical numerical realization in its own real scalar extension.

Equations

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

noncomputable def AlgebraicGeometry.Numerical.Surface.ScalarExtension.chernCharacter {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] {V : NumericalVarietyData 2 A N} : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter N (RealDivisorClass V.ring)

The full Chern character valued in the canonical real scalar extension of the rational codimension-one piece.

Equations

• AlgebraicGeometry.Numerical.Surface.ScalarExtension.chernCharacter = (AlgebraicGeometry.Numerical.Surface.scalarExtensionRealization V.ring).chernCharacter

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.ScalarExtension.chernCharacter_rank {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] {V : NumericalVarietyData 2 A N} (E : N) : chernCharacter.rank E = ↑(V.rank E)

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.ScalarExtension.chernCharacter_chOne {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] {V : NumericalVarietyData 2 A N} (E : N) : chernCharacter.chOne E = RealDivisorClass.ofRational V.ring ⟨V.chComp E 1, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Numerical.Surface.ScalarExtension.chernCharacter_chTwo {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] {V : NumericalVarietyData 2 A N} (E : N) : chernCharacter.chTwo E = ↑(V.ring.degree (V.chComp E 2))

theorem AlgebraicGeometry.Numerical.Surface.ScalarExtension.map_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.extendDivisorClass (chernCharacter.chOne E) = R.chernCharacter.chOne E

The concrete first Chern class is the image of the canonical scalar-extended first Chern class.

theorem AlgebraicGeometry.Numerical.Surface.ScalarExtension.centralCharge_eq_realization {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 : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters (RealDivisorClass V.ring)) (E : N) : (chernCharacter.centralCharge (RealDivisorClass.divisorSpace V.ring) P) E = (R.chernCharacter.centralCharge R.divisorSpace (R.realizeParameters P)) E

Arbitrary real scalar-extended B-fields and polarizations give the same central charge after transport to any concrete numerical divisor realization.