The homogeneous coordinate ring of a Weierstrass curve

For a Weierstrass curve W' over a commutative ring R, this file defines the homogeneous coordinate ring

R[X, Y, Z] ⧸ (Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³))

of the projective cubic, graded by total degree. Its Proj is the projective Weierstrass model WeierstrassCurve.projModel of TauCeti/AlgebraicGeometry/EllipticCurve/Scheme/ProjModel.lean. The grading is induced from the grading of R[X, Y, Z] by total degree, using TauCeti.GradedAlgebra.gradedAlgebraQuotientPiece.

Main definitions

• WeierstrassCurve.Projective.CoordinateRing W': the quotient of R[X, Y, Z] by the homogeneous Weierstrass polynomial W'.polynomial.
• WeierstrassCurve.Projective.grading W': its grading by total degree, registered as a GradedAlgebra instance.
• WeierstrassCurve.Projective.gradingZeroEquiv W': the degree-zero part of the coordinate ring is the base ring R.
• WeierstrassCurve.Projective.evalZero W': evaluation at the point [0 : 1 : 0].
• WeierstrassCurve.Projective.evalHom W' g hP: evaluation at a solution P of the projective equation of W'.map g, for a ring homomorphism g.
• WeierstrassCurve.Projective.coord W' i: the class of the homogeneous coordinate Xᵢ, of degree one.

Main results

• WeierstrassCurve.Projective.isHomogeneous_polynomial: the Weierstrass polynomial in projective coordinates is homogeneous of degree 3, so it cuts out a homogeneous ideal.
• WeierstrassCurve.Projective.bijective_algebraMap_grading_zero: the degree-zero part of the homogeneous coordinate ring is R; hence Proj of it lies over Spec R.
• WeierstrassCurve.Projective.irrelevant_le_span_range_coord: the three coordinates generate the irrelevant ideal, so the standard charts D₊(Xᵢ) cover Proj of the coordinate ring.
• WeierstrassCurve.Projective.equation_coord: the classes of the coordinates are a solution of the equation over the coordinate ring, nonzero over a nontrivial ring (coord_ne_zero).
• WeierstrassCurve.Projective.eq_evalHom and WeierstrassCurve.Projective.ringHom_ext: a ring homomorphism out of the coordinate ring is determined by its values on R and on the coordinates; evalHom is the one with prescribed values (evalHom_comp_algebraMap, evalHom_comp_coord).

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.

theorem WeierstrassCurve.Projective.isHomogeneous_polynomial {R : Type u_1} [CommRing R] (W' : Projective R) : W'.polynomial.IsHomogeneous 3

The Weierstrass polynomial Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³) in projective coordinates is homogeneous of degree 3.

@[reducible, inline]

abbrev WeierstrassCurve.Projective.CoordinateRing {R : Type u_1} [CommRing R] (W' : Projective R) : Type u_1

The homogeneous coordinate ring R[X, Y, Z] ⧸ (W'(X, Y, Z)) of the projective Weierstrass cubic.

Equations

• W'.CoordinateRing = (MvPolynomial (Fin 3) R ⧸ Ideal.span {W'.polynomial})

theorem WeierstrassCurve.Projective.isHomogeneous_span_polynomial {R : Type u_1} [CommRing R] (W' : Projective R) : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) R) (Ideal.span {W'.polynomial})

The ideal generated by the Weierstrass polynomial is homogeneous for the grading of R[X, Y, Z] by total degree.

noncomputable def WeierstrassCurve.Projective.grading {R : Type u_1} [CommRing R] (W' : Projective R) (n : ℕ) : Submodule R W'.CoordinateRing

The grading of the homogeneous coordinate ring by total degree: the degree-n part is the image of the homogeneous polynomials of degree n.

Equations

• W'.grading n = TauCeti.GradedAlgebra.quotientPiece (MvPolynomial.homogeneousSubmodule (Fin 3) R) (Ideal.span {W'.polynomial}) n

theorem WeierstrassCurve.Projective.mem_grading_iff {R : Type u_1} [CommRing R] (W' : Projective R) {n : ℕ} {x : W'.CoordinateRing} : x ∈ W'.grading n ↔ ∃ (p : MvPolynomial (Fin 3) R), p.IsHomogeneous n ∧ (Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p = x

Membership in a graded piece of the homogeneous coordinate ring is being the class of a homogeneous polynomial of that degree.

theorem WeierstrassCurve.Projective.mk_mem_grading {R : Type u_1} [CommRing R] (W' : Projective R) {n : ℕ} {p : MvPolynomial (Fin 3) R} (hp : p.IsHomogeneous n) : (Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p ∈ W'.grading n

The class of a homogeneous polynomial of degree n lies in the degree-n part.

@[instance_reducible]

noncomputable instance WeierstrassCurve.Projective.instGradedAlgebraNatCoordinateRingGrading {R : Type u_1} [CommRing R] (W' : Projective R) : GradedAlgebra W'.grading

The homogeneous coordinate ring is graded by total degree.

Equations

• W'.instGradedAlgebraNatCoordinateRingGrading = id (TauCeti.GradedAlgebra.gradedAlgebraQuotientPiece (MvPolynomial.homogeneousSubmodule (Fin 3) R) (Ideal.span {W'.polynomial}) ⋯)

instance WeierstrassCurve.Projective.instFiniteTypeSubtypeCoordinateRingMemSubmoduleGradingOfNatNat {R : Type u_1} [CommRing R] (W' : Projective R) : Algebra.FiniteType (↥(W'.grading 0)) W'.CoordinateRing

The homogeneous coordinate ring is of finite type over its degree-zero part.

theorem WeierstrassCurve.Projective.bijective_algebraMap_grading_zero {R : Type u_1} [CommRing R] (W' : Projective R) : Function.Bijective ⇑(algebraMap R ↥(W'.grading 0))

The degree-zero part of the homogeneous coordinate ring is the base ring: the Weierstrass polynomial has no constant term, so no nonzero constant is a multiple of it, and the degree-zero polynomials are the constants.

noncomputable def WeierstrassCurve.Projective.gradingZeroEquiv {R : Type u_1} [CommRing R] (W' : Projective R) : R ≃ₐ[R] ↥(W'.grading 0)

The degree-zero part of the homogeneous coordinate ring is isomorphic to the base ring.

Equations

• W'.gradingZeroEquiv = AlgEquiv.ofBijective (Algebra.ofId R ↥(W'.grading 0)) ⋯

@[simp]

theorem WeierstrassCurve.Projective.gradingZeroEquiv_apply {R : Type u_1} [CommRing R] (W' : Projective R) (r : R) : W'.gradingZeroEquiv r = (algebraMap R ↥(W'.grading 0)) r

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Projective.coord {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : W'.CoordinateRing

The class of the homogeneous coordinate Xᵢ in the homogeneous coordinate ring.

Equations

• W'.coord i = (Ideal.Quotient.mk (Ideal.span {W'.polynomial})) (MvPolynomial.X i)

theorem WeierstrassCurve.Projective.coord_mem_grading {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : W'.coord i ∈ W'.grading 1

Each homogeneous coordinate has degree one.

theorem WeierstrassCurve.Projective.irrelevant_le_span_range_coord {R : Type u_1} [CommRing R] (W' : Projective R) : (HomogeneousIdeal.irrelevant W'.grading).toIdeal ≤ Ideal.span (Set.range W'.coord)

The irrelevant ideal of the homogeneous coordinate ring is generated by the three coordinates: every homogeneous element of positive degree is the class of a polynomial without constant term.

noncomputable def WeierstrassCurve.Projective.evalZero {R : Type u_1} [CommRing R] (W' : Projective R) : W'.CoordinateRing →ₐ[R] R

Evaluation of the homogeneous coordinate ring at the point [0 : 1 : 0].

Equations

• W'.evalZero = Ideal.Quotient.liftₐ (Ideal.span {W'.polynomial}) (MvPolynomial.aeval ![0, 1, 0]) ⋯

@[simp]

theorem WeierstrassCurve.Projective.evalZero_mk {R : Type u_1} [CommRing R] (W' : Projective R) (p : MvPolynomial (Fin 3) R) : W'.evalZero ((Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p) = (MvPolynomial.eval ![0, 1, 0]) p

instance WeierstrassCurve.Projective.instFaithfulSMulCoordinateRing {R : Type u_1} [CommRing R] (W' : Projective R) : FaithfulSMul R W'.CoordinateRing

The base ring acts faithfully on the homogeneous coordinate ring, as on the affine coordinate ring WeierstrassCurve.Affine.CoordinateRing.

noncomputable def WeierstrassCurve.Projective.evalHom {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) : W'.CoordinateRing →+* S

Evaluation of the homogeneous coordinate ring at a solution P of the projective Weierstrass equation of W'.map g, for a ring homomorphism g : R →+* S: the ring homomorphism R[X₀, X₁, X₂] ⧸ (W'(X₀, X₁, X₂)) →+* S that is g on R and sends the class of Xᵢ to Pᵢ.

Equations

• W'.evalHom g hP = Ideal.Quotient.lift (Ideal.span {W'.polynomial}) (MvPolynomial.eval₂Hom g P) ⋯

@[simp]

theorem WeierstrassCurve.Projective.evalHom_mk {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) (p : MvPolynomial (Fin 3) R) : (W'.evalHom g hP) ((Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p) = MvPolynomial.eval₂ g P p

evalHom sends the class of a polynomial p to its value p(P), the coefficients of p being mapped to S by g.

theorem WeierstrassCurve.Projective.evalHom_comp_algebraMap {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) : (W'.evalHom g hP).comp (algebraMap R W'.CoordinateRing) = g

evalHom restricts to g on the base ring R.

theorem WeierstrassCurve.Projective.evalHom_comp_coord {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) : ⇑(W'.evalHom g hP) ∘ W'.coord = P

evalHom sends the class of each coordinate Xᵢ to Pᵢ.

theorem WeierstrassCurve.Projective.map_evalHom {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) : (W'.map (algebraMap R W'.CoordinateRing)).map (W'.evalHom g hP) = W'.map g

Pushing the curve over the homogeneous coordinate ring forward along evalHom gives the curve W'.map g.

theorem WeierstrassCurve.Projective.ringHom_ext {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] {f₁ f₂ : W'.CoordinateRing →+* S} (h₁ : f₁.comp (algebraMap R W'.CoordinateRing) = f₂.comp (algebraMap R W'.CoordinateRing)) (h₂ : ⇑f₁ ∘ W'.coord = ⇑f₂ ∘ W'.coord) : f₁ = f₂

Two ring homomorphisms out of the homogeneous coordinate ring are equal when they agree on the base ring and on the classes of the coordinates.

theorem WeierstrassCurve.Projective.eq_evalHom {R : Type u_1} [CommRing R] (W' : Projective R) {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) {f : W'.CoordinateRing →+* S} (h₁ : f.comp (algebraMap R W'.CoordinateRing) = g) (h₂ : ⇑f ∘ W'.coord = P) : f = W'.evalHom g hP

evalHom is the only ring homomorphism out of the homogeneous coordinate ring that restricts to g on R and sends the class of each coordinate Xᵢ to Pᵢ.

theorem WeierstrassCurve.Projective.equation_coord {R : Type u_1} [CommRing R] (W' : Projective R) : (W'.map (algebraMap R W'.CoordinateRing)).Equation W'.coord

The classes of the homogeneous coordinates form a solution of the Weierstrass equation over the homogeneous coordinate ring.

theorem WeierstrassCurve.Projective.coord_ne_zero {R : Type u_1} [CommRing R] (W' : Projective R) [Nontrivial R] : W'.coord ≠ 0

Over a nontrivial ring, the solution given by the classes of the homogeneous coordinates is nonzero.