Coordinate-free elliptic-curve dictionary

This file restates the elliptic function-field place dictionary and degree-one Picard torsor over intrinsic places. The former two-chart implementation remains in WeierstrassCurve.Affine.Chart.

noncomputable def WeierstrassCurve.Affine.infinityPlace {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : FunctionField.Place k K

The intrinsic infinity place of an elliptic function field.

Equations

• WeierstrassCurve.Affine.infinityPlace K = (FunctionField.chartToPlace k K) (WeierstrassCurve.Affine.Chart.infinityPlace K)

noncomputable def WeierstrassCurve.Affine.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] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (P : W.Point) : FunctionField.Place k K

The intrinsic place associated to a Weierstrass point.

Equations

• W.placeOfPoint K P = (FunctionField.chartToPlace k K) (WeierstrassCurve.Affine.Chart.placeOfPoint W K P)

theorem WeierstrassCurve.Affine.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] [Algebra k K] [IsScalarTower k (Polynomial k) K] (P : W.Point) : (W.placeOfPoint K P).degree = 1

Every Weierstrass point gives a degree-one intrinsic place.

theorem WeierstrassCurve.Affine.infinityPlace_deg_one {k : Type u_1} [Field k] (W : Affine k) (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] [Algebra k K] [IsScalarTower k (Polynomial k) K] : (infinityPlace K).degree = 1

The intrinsic infinity place has degree one.

noncomputable def WeierstrassCurve.Affine.degreeOnePlaceEquivChart {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : { v : FunctionField.Place k K // v.degree = 1 } ≃ { w : FunctionField.Chart.PlaceA k K // FunctionField.Chart.placeDegree k K w = 1 }

Degree-one intrinsic places are equivalent to degree-one coordinate places.

Equations

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

theorem WeierstrassCurve.Affine.exists_point_of_place_degree_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] [Algebra k K] [IsScalarTower k (Polynomial k) K] (v : FunctionField.Place k K) (hv : v.degree = 1) : ∃ (P : W.Point), v = W.placeOfPoint K P

Every degree-one intrinsic place comes from a Weierstrass point.

theorem WeierstrassCurve.Affine.genus_eq_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] [Algebra k K] [IsScalarTower k (Polynomial k) K] [FunctionField.IsFullConstantField k K] : FunctionField.genus k K = 1

The genus of an elliptic function field is one, in the intrinsic API.

noncomputable def WeierstrassCurve.Affine.picTorsor {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] [Algebra k K] [IsScalarTower k (Polynomial k) K] [FunctionField.IsFullConstantField k K] : { v : FunctionField.Place k K // v.degree = 1 } ≃ ClassGroup W.CoordinateRing

The degree-one intrinsic places form the Picard torsor of the elliptic coordinate ring.

Equations

• W.picTorsor K = (WeierstrassCurve.Affine.degreeOnePlaceEquivChart K).trans (WeierstrassCurve.Affine.Chart.Internal.picTorsor' W K)

theorem WeierstrassCurve.Affine.picTorsor_compat_groupLaw {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] [Algebra k K] [IsScalarTower k (Polynomial k) K] [FunctionField.IsFullConstantField k K] {x y : k} (h : W.Nonsingular x y) : (W.picTorsor K) ⟨W.placeOfPoint K (Point.some x y h), ⋯⟩ = (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

Compatibility with Angdinata's group law in the intrinsic place API.