The standard affine charts of the projective Weierstrass cubic

For a Weierstrass curve W' over R and a homogeneous coordinate Xᵢ, the standard affine chart D₊(Xᵢ) of the projective cubic is the spectrum of the degree-zero part A_(Xᵢ) of the localization of the homogeneous coordinate ring A = R[X₀, X₁, X₂] ⧸ (W(X₀, X₁, X₂)) away from Xᵢ. This file identifies A_(Xᵢ) with the dehomogenized ring

R[X₀, X₁, X₂] ⧸ (W(X₀, X₁, X₂), Xᵢ - 1),

the fraction a / Xᵢⁿ corresponding to the class of a with Xᵢ set to 1. Keeping all three variables and adding the relation Xᵢ - 1 treats the three charts uniformly, and presents each chart by three generators and two relations; this is the form in which the smoothness of the projective model is checked.

Main definitions

• WeierstrassCurve.Projective.chartRelation W' i: the two relations W(X₀, X₁, X₂) and Xᵢ - 1.
• WeierstrassCurve.Projective.ChartRing W' i: the quotient of R[X₀, X₁, X₂] by them.
• WeierstrassCurve.Projective.awayEquivChartRing W' i: the isomorphism A_(Xᵢ) ≃+* ChartRing.
• WeierstrassCurve.Projective.chartPoint W' i: the universal point of the chart, whose coordinates are the classes of X₀, X₁, X₂ in ChartRing W' i.
• WeierstrassCurve.Projective.awayEvalHom W' g hP hi: the homomorphism A_(Xᵢ) →+* S, a / Xᵢⁿ ↦ a(P) / Pᵢⁿ, at a solution P of the equation of W'.map g with Pᵢ a unit.

Main results

• WeierstrassCurve.Projective.awayEquivChartRing_mk: the isomorphism sends a / Xᵢⁿ to the class of a.
• WeierstrassCurve.Projective.awayEquivChartRing_symm_comp_algebraMap: the isomorphism is compatible with the structure maps from R.
• WeierstrassCurve.Projective.equation_chartPoint: the universal point of the chart is a solution of the Weierstrass equation over ChartRing W' i.

References

• [R. Hartshorne, Algebraic Geometry, II.2.5][hartshorne1977]

Provenance

chartPoint and equation_chartPoint are adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/AdditionChartRing.lean (affineChartPoint and equation_affineChartPoint), stated for TauCeti's ChartRing.

noncomputable def WeierstrassCurve.Projective.chartRelation {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : Fin 2 → MvPolynomial (Fin 3) R

The two relations W(X₀, X₁, X₂) and Xᵢ - 1 cutting out the standard affine chart Xᵢ ≠ 0 of the projective Weierstrass cubic, as a closed subscheme of affine 3-space.

Equations

• W'.chartRelation i = ![W'.polynomial, MvPolynomial.X i - 1]

@[simp]

theorem WeierstrassCurve.Projective.chartRelation_zero {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : W'.chartRelation i 0 = W'.polynomial

@[simp]

theorem WeierstrassCurve.Projective.chartRelation_one {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : W'.chartRelation i 1 = MvPolynomial.X i - 1

@[reducible, inline]

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

The coordinate ring R[X₀, X₁, X₂] ⧸ (W(X₀, X₁, X₂), Xᵢ - 1) of the standard affine chart Xᵢ ≠ 0 of the projective Weierstrass cubic.

Equations

• W'.ChartRing i = (MvPolynomial (Fin 3) R ⧸ Ideal.span (Set.range (W'.chartRelation i)))

noncomputable def WeierstrassCurve.Projective.awayEquivChartRing {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : HomogeneousLocalization.Away W'.grading (W'.coord i) ≃+* W'.ChartRing i

The degree-zero part A_(Xᵢ) of the localization of the homogeneous coordinate ring away from Xᵢ is the coordinate ring R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1) of the standard affine chart.

Equations

• W'.awayEquivChartRing i = RingEquiv.ofRingHom (WeierstrassCurve.Projective.awayToChartRing✝ W' i) (WeierstrassCurve.Projective.chartRingToAway✝ W' i) ⋯ ⋯

@[simp]

theorem WeierstrassCurve.Projective.awayEquivChartRing_mk {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) {n : ℕ} {p : MvPolynomial (Fin 3) R} (hp : (Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p ∈ W'.grading (n • 1)) : (W'.awayEquivChartRing i) (HomogeneousLocalization.Away.mk W'.grading ⋯ n ((Ideal.Quotient.mk (Ideal.span {W'.polynomial})) p) hp) = (Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) p

awayEquivChartRing sends a / Xᵢⁿ to the class of a with Xᵢ set to 1.

@[simp]

theorem WeierstrassCurve.Projective.awayEquivChartRing_symm_mk_X {R : Type u_1} [CommRing R] (W' : Projective R) (i j : Fin 3) : (W'.awayEquivChartRing i).symm ((Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) (MvPolynomial.X j)) = HomogeneousLocalization.Away.mk W'.grading ⋯ 1 (W'.coord j) ⋯

The inverse of awayEquivChartRing sends the class of Xⱼ to the fraction Xⱼ / Xᵢ.

theorem WeierstrassCurve.Projective.awayEquivChartRing_symm_comp_algebraMap {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : (W'.awayEquivChartRing i).symm.toRingHom.comp (algebraMap R (W'.ChartRing i)) = (HomogeneousLocalization.fromZeroRingHom W'.grading (Submonoid.powers (W'.coord i))).comp (algebraMap R ↥(W'.grading 0))

awayEquivChartRing is compatible with the structure maps from R: on the chart ring it is the quotient map, on A_(Xᵢ) it factors through the degree-zero part of the coordinate ring.

@[simp]

theorem WeierstrassCurve.Projective.chartRing_mk_X_self {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : (Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) (MvPolynomial.X i) = 1

In the chart ring ChartRing W' i, the class of the coordinate Xᵢ is 1.

noncomputable def WeierstrassCurve.Projective.chartPoint {R : Type u_1} [CommRing R] (W' : Projective R) (i a✝ : Fin 3) : W'.ChartRing i

The universal point of the standard affine chart D₊(Xᵢ) of the projective Weierstrass cubic: the classes of the three homogeneous coordinates in ChartRing W' i.

Equations

• W'.chartPoint i k = (Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) (MvPolynomial.X k)

@[simp]

theorem WeierstrassCurve.Projective.chartPoint_apply {R : Type u_1} [CommRing R] (W' : Projective R) (i k : Fin 3) : W'.chartPoint i k = (Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) (MvPolynomial.X k)

The coordinates of the universal point of the chart D₊(Xᵢ) are the classes of X₀, X₁, X₂.

theorem WeierstrassCurve.Projective.chartPoint_self {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : W'.chartPoint i i = 1

The i-th coordinate of the universal point of the chart D₊(Xᵢ) is 1.

theorem WeierstrassCurve.Projective.equation_chartPoint {R : Type u_1} [CommRing R] (W' : Projective R) (i : Fin 3) : (W'.baseChange (W'.ChartRing i)).Equation (W'.chartPoint i)

The universal point of the chart D₊(Xᵢ) is a solution of the Weierstrass equation over ChartRing W' i.

noncomputable def WeierstrassCurve.Projective.awayEvalHom {R : Type u_1} [CommRing R] (W' : Projective R) {i : Fin 3} {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) (hi : IsUnit (P i)) : HomogeneousLocalization.Away W'.grading (W'.coord i) →+* S

The ring homomorphism A_(Xᵢ) →+* S, a / Xᵢⁿ ↦ a(P) / Pᵢⁿ (awayEvalHom_mk), on the degree-zero part A_(Xᵢ) of the localization of the homogeneous coordinate ring away from Xᵢ, at a solution P of the projective Weierstrass equation of W'.map g whose coordinate Pᵢ is a unit. It restricts to g on R (awayEvalHom_comp_algebraMap).

Equations

• W'.awayEvalHom g hP hi = HomogeneousLocalization.Away.lift W'.grading (W'.evalHom g hP) ⋯

theorem WeierstrassCurve.Projective.awayEvalHom_def {R : Type u_1} [CommRing R] (W' : Projective R) {i : Fin 3} {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) (hi : IsUnit (P i)) : W'.awayEvalHom g hP hi = HomogeneousLocalization.Away.lift W'.grading (W'.evalHom g hP) ⋯

awayEvalHom is the homomorphism HomogeneousLocalization.Away.lift induced by the evaluation evalHom of the homogeneous coordinate ring at P.

@[simp]

theorem WeierstrassCurve.Projective.awayEvalHom_mk {R : Type u_1} [CommRing R] (W' : Projective R) {i : Fin 3} {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) (hi : IsUnit (P i)) (n : ℕ) (a : W'.CoordinateRing) (ha : a ∈ W'.grading (n • 1)) : (W'.awayEvalHom g hP hi) (HomogeneousLocalization.Away.mk W'.grading ⋯ n a ha) = (W'.evalHom g hP) a * ↑(hi.unit ^ n)⁻¹

awayEvalHom sends the fraction a / Xᵢⁿ to a(P) / Pᵢⁿ.

theorem WeierstrassCurve.Projective.awayEvalHom_comp_algebraMap {R : Type u_1} [CommRing R] (W' : Projective R) {i : Fin 3} {S : Type u_2} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W'.map g).Equation P) (hi : IsUnit (P i)) : (W'.awayEvalHom g hP hi).comp ((HomogeneousLocalization.fromZeroRingHom W'.grading (Submonoid.powers (W'.coord i))).comp (algebraMap R ↥(W'.grading 0))) = g

awayEvalHom restricts to g on the base ring R, which maps to A_(Xᵢ) through the degree-zero part of the homogeneous coordinate ring.