Place–point dictionary for Weierstrass function fields

For an elliptic Weierstrass curve W/k, affine nonsingular points should correspond to degree-one places, with a unique degree-one place at infinity.

Following the ClassGroup.mk design, the function field is an abstract field K linked to the curve by [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K], carrying the The coordinate instance pack. Working over the concrete FractionRing W.CoordinateRing would tie every statement to one Semiring derivation path and break instance unification (OreLocalization.instSemiring vs FractionRing.field).

Finite places

noncomputable def WeierstrassCurve.Affine.Chart.coordinateRingEquivIntegers {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] : W.CoordinateRing ≃ₐ[Polynomial k] ↥(FunctionField.ringOfIntegers k K)

The integral-closure identification between the affine coordinate ring and the finite-integer ring of its fraction field.

Equations

• WeierstrassCurve.Affine.Chart.coordinateRingEquivIntegers W K = IsIntegralClosure.equiv (Polynomial k) W.CoordinateRing K ↥(FunctionField.ringOfIntegers k K)

theorem WeierstrassCurve.Affine.Chart.XYIdeal_isMaximal {k : Type u_1} [Field k] (W : Affine k) {x y : k} (h : W.Nonsingular x y) : (CoordinateRing.XYIdeal W x (Polynomial.C y)).IsMaximal

The ideal of a nonsingular affine point is maximal.

theorem WeierstrassCurve.Affine.Chart.XYIdeal_ne_bot {k : Type u_1} [Field k] (W : Affine k) {x y : k} (_h : W.Nonsingular x y) : CoordinateRing.XYIdeal W x (Polynomial.C y) ≠ ⊥

The ideal of an affine point is nonzero.

noncomputable def WeierstrassCurve.Affine.Chart.affineHeightOne {k : Type u_1} [Field k] (W : Affine k) {x y : k} (h : W.Nonsingular x y) : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing

A nonsingular affine point as a height-one prime of the coordinate ring.

Equations

• WeierstrassCurve.Affine.Chart.affineHeightOne W h = { asIdeal := WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y), isPrime := ⋯, ne_bot := ⋯ }

noncomputable def WeierstrassCurve.Affine.Chart.finitePlaceOfAffine {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] {x y : k} (h : W.Nonsingular x y) : FunctionField.Chart.PlaceA k K

The finite place corresponding to a nonsingular affine pair.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Affine.Chart.finitePlaceOfAffine_degree {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] {x y : k} (h : W.Nonsingular x y) : FunctionField.Chart.placeDegree k K (finitePlaceOfAffine W K h) = 1

A rational affine point gives a degree-one finite place.

theorem WeierstrassCurve.Affine.Chart.maximal_eq_XYIdeal {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] [IsAlgClosed k] (I : Ideal W.CoordinateRing) [I.IsMaximal] : ∃ (x : k) (y : k) (_ : W.Nonsingular x y), I = CoordinateRing.XYIdeal W x (Polynomial.C y)

Over an algebraically closed field, every maximal ideal of the affine coordinate ring is the ideal of a nonsingular rational point.

noncomputable def WeierstrassCurve.Affine.Chart.placeOfPoint {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] : W.Point → FunctionField.Chart.PlaceA k K

The finite place corresponding to a nonsingular affine point (x, y).

Equations

• WeierstrassCurve.Affine.Chart.placeOfPoint W K WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Chart.infinityPlace K
• WeierstrassCurve.Affine.Chart.placeOfPoint W K (WeierstrassCurve.Affine.Point.some x_1 y h) = WeierstrassCurve.Affine.Chart.finitePlaceOfAffine W K h

theorem WeierstrassCurve.Affine.Chart.placeOfPoint_deg_one {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (P : W.Point) : FunctionField.Chart.placeDegree k K (placeOfPoint W K P) = 1

theorem WeierstrassCurve.Affine.Chart.place_dichotomy {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsAlgClosed k] (v : FunctionField.Chart.PlaceA k K) : (∃ (P : W.Point), v = placeOfPoint W K P) ∨ v = infinityPlace K