LeanPool.CCDN.Projection.CurvePrimitivePair

Bounded linear coordinates generating an affine curve's function field. Degree preservation and control of exceptional fibers are separate projection obligations; this module proves the quantified birational input.

source

noncomputable def CCDN.momentCoordinate (K : Type u_1) [CommRing K] (n k : ℕ) :

MvPolynomial (Fin n) K

The bounded integer moment-curve linear form.

Equations

CCDN.momentCoordinate K n k = ∑ j : Fin n, MvPolynomial.C (↑k ^ ↑j) * MvPolynomial.X j

Instances For

source

theorem CCDN.momentCoordinate_degree (K : Type u_1) [CommRing K] [Nontrivial K] (n k : ℕ) :

(momentCoordinate K n k).totalDegree ≤ 1

The moment coordinate has total degree at most one.

source

theorem CCDN.momentCoordinate_fraction {K : Type u_1} {F : Type u_2} [Field K] [Field F] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [Algebra (MvPolynomial (Fin n) K ⧸ I) F] (k : ℕ) :

(algebraMap (MvPolynomial (Fin n) K ⧸ I) F) ((Ideal.Quotient.mk I) (momentCoordinate K n k)) = ∑ j : Fin n, (algebraMap (MvPolynomial (Fin n) K ⧸ I) F) ((Ideal.Quotient.mk I) (MvPolynomial.X j)) * ↑k ^ ↑j

In any field F receiving the quotient by I compatibly with K, the image of the moment coordinate with parameter k is ∑ j, x j * k ^ j, where x j is the image of X j.