Points of the projective model and places of the function field

Let W be an elliptic Weierstrass curve over a field K and let E = projModel W be its projective model, a smooth proper curve over K. This file shows that the function field of E is an algebraic function field of one variable over K, and identifies the codimension-one points of E with the places of the function field K(W) of the affine equation: a point goes to the place whose valuation ring is its local ring, transported along WeierstrassCurve.projModelFunctionFieldEquiv.

Under this identification the zero section O = [0 : 1 : 0] is the place at infinity. The coordinate x is regular at every point of the chart D₊(Z), so no point of D₊(Z) gives the place at infinity, where x has a pole; the complement of D₊(Z) is the single point O.

Main declarations

• WeierstrassCurve.isFunctionField_functionField_projModel: K(E) is a function field over K;
• WeierstrassCurve.projModelCodimensionOnePointEquivPlace: the codimension-one points of projModel W are the places of K(W);
• WeierstrassCurve.mem_integers_projModelCodimensionOnePointEquivPlace_iff: the valuation ring of the place of a point is its local ring;
• WeierstrassCurve.degree_projModelCodimensionOnePointEquivPlace: the degree of the place of a point is its residue degree.
• WeierstrassCurve.projModelZeroPoint: the zero section O, as a codimension-one point.
• WeierstrassCurve.projModelCodimensionOnePointEquivPlace_projModelZeroPoint: the place of O is the place at infinity.

References

• R. Hartshorne, Algebraic Geometry, Chapter I, Section 6, and Chapter II, Section 6.

theorem WeierstrassCurve.projModelFunctionFieldEquiv_algebraMap {K : Type u} [Field K] (W : WeierstrassCurve K) (c : K) : W.projModelFunctionFieldEquiv ((algebraMap K ↑W.projModel.functionField) c) = (algebraMap K W.toAffine.FunctionField) ((RingEquiv.refl K) c)

The function-field comparison projModelFunctionFieldEquiv respects the constants, for the algebra structure on K(E) defined by the structure morphism. It is stated in the form of the compatibility hypothesis of Place.equivOfRingEquiv for the identity of K.

theorem WeierstrassCurve.isFunctionField_functionField_projModel {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : TauCeti.IsFunctionField K ↑W.projModel.functionField

The function field of the projective model of an elliptic curve is an algebraic function field of one variable over the base field.

noncomputable def WeierstrassCurve.projModelCodimensionOnePointEquivPlace {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : TauCeti.AlgebraicGeometry.CodimensionOnePoint W.projModel ≃ TauCeti.Place K W.toAffine.FunctionField

The codimension-one points of the projective model are the places of K(W). A codimension-one point of E = projModel W goes to the place of K(E) whose valuation ring is its local ring, transported to K(W) along projModelFunctionFieldEquiv.

theorem WeierstrassCurve.projModelCodimensionOnePointEquivPlace_apply {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint W.projModel) : W.projModelCodimensionOnePointEquivPlace y = (TauCeti.Place.equivOfRingEquiv (RingEquiv.refl K) W.projModelFunctionFieldEquiv ⋯) (W.projModel.toPlace ↑y)

The place attached to a codimension-one point y of projModel W is the transport along projModelFunctionFieldEquiv of the place of K(E) at y.

theorem WeierstrassCurve.mem_integers_projModelCodimensionOnePointEquivPlace_iff {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint W.projModel) (z : W.toAffine.FunctionField) : z ∈ (W.projModelCodimensionOnePointEquivPlace y).integers ↔ ∃ (a : ↑(W.projModel.presheaf.stalk ↑y)), W.projModelFunctionFieldEquiv ((algebraMap ↑(W.projModel.presheaf.stalk ↑y) ↑W.projModel.functionField) a) = z

The valuation ring of the place of a point is its local ring: a function of K(W) is integral at the place attached to a codimension-one point y of projModel W exactly when it comes from the local ring of projModel W at y.

@[simp]

theorem WeierstrassCurve.degree_projModelCodimensionOnePointEquivPlace {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint W.projModel) : (W.projModelCodimensionOnePointEquivPlace y).degree = AlgebraicGeometry.Scheme.Hom.residueDegree (W.projModel ↘ AlgebraicGeometry.Spec ↧K) ↑y

The degree of the place attached to a codimension-one point of projModel W is the residue degree of the point over the base field.

noncomputable def WeierstrassCurve.projModelZeroPoint {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : TauCeti.AlgebraicGeometry.CodimensionOnePoint W.projModel

The zero section O of the projective model of an elliptic curve, as a codimension-one point: a rational point of a curve has codimension one.

@[simp]

theorem WeierstrassCurve.coe_projModelZeroPoint {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : ↑W.projModelZeroPoint = W.projModelZero (IsLocalRing.closedPoint K)

The point O is the image of the zero section.

@[simp]

theorem WeierstrassCurve.projModelCodimensionOnePointEquivPlace_projModelZeroPoint {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : W.projModelCodimensionOnePointEquivPlace W.projModelZeroPoint = TauCeti.Place.infinity W.toAffine

The point O of the projective model is the place at infinity: the codimension-one point O = [0 : 1 : 0] corresponds to the place at infinity of K(W).

theorem WeierstrassCurve.valuation_toPlace_projModelZeroPoint {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : (W.projModel.toPlace ↑W.projModelZeroPoint).valuation = Valuation.comap (↑W.projModelFunctionFieldEquiv) W.toAffine.infinityPlace

The valuation of the place of the point O is the valuation at infinity, read through the identification of function fields.