The monomial basis of the coordinate ring of a Weierstrass curve

Let W be a Weierstrass curve over a commutative ring R, and let x and y be the coordinate functions of its affine coordinate ring R[W] = R[X, Y] ⧸ (W(X, Y)). Mathlib provides the basis {1, y} of R[W] over R[X], WeierstrassCurve.Affine.CoordinateRing.basis. Together with the monomial basis of R[X] over R it gives a basis of R[W] over R itself: the monomials xⁱ and xⁱy.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.basisMonomials: the basis of R[W] over R formed by the monomials xⁱ and xⁱy.

Main results

• WeierstrassCurve.Affine.CoordinateRing.basisMonomials_apply: the basis vector at (i, j) is the monomial xⁱyʲ.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/PoleFiltration.lean. basisMonomials is the definition of the private coordinateRingMonomialBasis of that file; the source has no lemma for its general value.

noncomputable def WeierstrassCurve.Affine.CoordinateRing.basisMonomials {R : Type u_1} [CommRing R] (W : Affine R) : Module.Basis (ℕ × Fin 2) R W.CoordinateRing

The monomials xⁱ and xⁱy in the coordinate functions x and y form a basis of the coordinate ring R[W] over the base ring R: the basis vector at (i, j) : ℕ × Fin 2 is xⁱyʲ. See WeierstrassCurve.Affine.CoordinateRing.basis for the basis {1, y} of R[W] over R[X].

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.basisMonomials_apply {R : Type u_1} [CommRing R] (W : Affine R) (i : ℕ) (j : Fin 2) : (CoordinateRing.basisMonomials W) (i, j) = (AdjoinRoot.of W.polynomial) Polynomial.X ^ i * AdjoinRoot.root W.polynomial ^ ↑j

The basis vector of CoordinateRing.basisMonomials at (i, j) is the monomial xⁱyʲ. The coordinate functions x and y are written AdjoinRoot.of W.polynomial X and AdjoinRoot.root W.polynomial, the simp normal forms of CoordinateRing.mk W (C X) and CoordinateRing.mk W Y.