Dimension-specific comparisons for polarised wall transport

This module imports the generic (n,m,κ) transport together with its surface and threefold specializations. The generic root imports neither specialization.

theorem AlgebraicGeometry.Numerical.Polarised.surface_toNumClass_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : Surface.toNumClass V P E = (hDegrees V P (unitCorr A) 2 E 0, hDegrees V P (unitCorr A) 2 E 1, hDegrees V P (unitCorr A) 2 E 2)

theorem AlgebraicGeometry.Numerical.Polarised.threefold_toNumClass_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : Threefold.toNumClass V P E = (hDegrees V P (unitCorr A) 3 E 0, hDegrees V P (unitCorr A) 3 E 1, hDegrees V P (unitCorr A) 3 E 2, hDegrees V P (unitCorr A) 3 E 3)

theorem AlgebraicGeometry.Numerical.Polarised.surfaceVec_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.surfaceVec (Surface.toNumClass V P E) = hDegrees V P (unitCorr A) 2 E

theorem AlgebraicGeometry.Numerical.Polarised.surface_wallChargeFamily_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) : Surface.wallChargeFamily V P = (wallChargeFamily V P (unitCorr A) 2).reindex CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.stChart