Constructing a NumericalRingData from a graded basis

The generic weighted-basis decomposition belongs to DerivedAlgGeo.LinearAlgebra.GradedBasis. This geometric consumer combines that decomposition with a top-degree functional to construct the numerical intersection-ring presentation NumericalRingData.

Given a basis b : Module.Basis ι ℚ A and a weight w : ι → ℕ bounded by n, the caller supplies three finite checks: that 1 lies in weight zero, that products of basis vectors respect weights, and that the degree map kills every basis vector outside top weight. The generic linear-algebra root supplies internality and vanishing above n.

@[reducible]

noncomputable def AlgebraicGeometry.Numerical.NumericalRingData.ofGradedBasis {ι : Type v} {A : Type u} [CommRing A] [Algebra ℚ A] (n : ℕ) (b : Module.Basis ι ℚ A) (w : ι → ℕ) (hw : ∀ (i : ι), w i ≤ n) (hone : 1 ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑b) w 0) (hmul : ∀ (p q : ι), b p * b q ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑b) w (w p + w q)) (deg : A →ₗ[ℚ] ℚ) (hdeg : ∀ (i : ι), w i ≠ n → deg (b i) = 0) : NumericalRingData n A

Build a NumericalRingData from a graded basis.

The caller supplies the basis, the weight function, and three finite checks: that 1 sits in codimension zero, that products of basis vectors respect the grading, and that the degree map kills every piece but the top one.

Equations

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

Smoke test

This exercises every hypothesis of ofGradedBasis on the dimension-zero intersection ring ℚ of a point. The exported point presentation is built independently in Numerical/Models/DimensionZero/Point.lean.