Points of a Weierstrass formal group in an adic ideal

Let I be an adic ideal of a complete linearly topologised ring O. The elements of I form an additive commutative group under evaluation of the Weierstrass formal group law: addition is F(t₁, t₂) and negation is the formal inverse ι(t). This file packages that group as WeierstrassCurve.FormalGroupPoint W I.

The wrapper is necessary because the subtype I already carries the ordinary addition inherited from O, whereas the addition here is the generally different formal-group operation. The assumption that I is adic is carried as Fact (IsAdic I): it makes every parameter evaluable and keeps addition and negation inside I.

This is only the parameter group. Mapping it into the points of the Weierstrass curve uses WeierstrassCurve.formalPoint; proving that map additive requires comparing the formal law with the geometric chord-and-tangent law.

Main definitions

• WeierstrassCurve.FormalGroupPoint: a parameter in an adic ideal, equipped with the Weierstrass formal group law.

Main results

• WeierstrassCurve.FormalGroupPoint.instAddCommGroup: the evaluated formal law makes these parameters an additive commutative group.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.1.

Provenance

The packaging follows Michael Stoll's elliptic-curve development (github.com/MichaelStollBayreuth/EllipticCurves @ 66889eada51a, Apache-2.0), file EllipticCurves/Mathlib/Chabauty/FormalGroupLaw/Points.lean, definition ChabautyColeman.FormalGroupLaw.Points and its AddCommMonoid instance. That source treats a multivariable formal group law on the maximal ideal of a local ring and does not construct inverses. Here the one-dimensional Weierstrass law is evaluated on an arbitrary adic ideal, and its already-constructed formal inverse upgrades the result to an additive commutative group.

structure WeierstrassCurve.FormalGroupPoint {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) (I : Ideal O) : Type u_1

A point of the formal group of a Weierstrass curve, with parameter in the adic ideal I.

This is a newtype rather than the ideal subtype itself: I already uses the ordinary addition of O, while FormalGroupPoint W I uses evaluation of W.formalAdd.

• val : O

  The parameter of a formal-group point.

• property : self.val ∈ I

  The parameter belongs to the ideal on which the formal law is evaluated.

theorem WeierstrassCurve.FormalGroupPoint.ext {O : Type u_1} {inst✝ : CommRing O} {W : WeierstrassCurve O} {I : Ideal O} {x y : W.FormalGroupPoint I} (val : x.val = y.val) : x = y

theorem WeierstrassCurve.FormalGroupPoint.ext_iff {O : Type u_1} {inst✝ : CommRing O} {W : WeierstrassCurve O} {I : Ideal O} {x y : W.FormalGroupPoint I} : x = y ↔ x.val = y.val

@[instance_reducible]

instance WeierstrassCurve.FormalGroupPoint.instCoeOut {O : Type u_1} [CommRing O] {W : WeierstrassCurve O} {I : Ideal O} : CoeOut (W.FormalGroupPoint I) O

A formal-group point coerces to its parameter in the coefficient ring.

Equations

• WeierstrassCurve.FormalGroupPoint.instCoeOut = { coe := WeierstrassCurve.FormalGroupPoint.val }

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_mk {O : Type u_1} [CommRing O] {W : WeierstrassCurve O} {I : Ideal O} (t : O) (ht : t ∈ I) : { val := t, property := ht }.val = t

The parameter of a formal-group point constructed from t is t.

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_inj {O : Type u_1} [CommRing O] {W : WeierstrassCurve O} {I : Ideal O} {P Q : W.FormalGroupPoint I} : P.val = Q.val ↔ P = Q

Two formal-group points are equal exactly when their parameters are equal.

theorem WeierstrassCurve.FormalGroupPoint.hasEval {O : Type u_1} [CommRing O] [UniformSpace O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] (P : W.FormalGroupPoint I) : PowerSeries.HasEval P.val

A parameter in an adic ideal is an admissible evaluation point for a power series.

@[instance_reducible]

instance WeierstrassCurve.FormalGroupPoint.instZero {O : Type u_1} [CommRing O] {W : WeierstrassCurve O} {I : Ideal O} : Zero (W.FormalGroupPoint I)

The zero parameter is the identity formal-group point.

Equations

• WeierstrassCurve.FormalGroupPoint.instZero = { zero := { val := 0, property := ⋯ } }

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_zero {O : Type u_1} [CommRing O] {W : WeierstrassCurve O} {I : Ideal O} : val 0 = 0

@[instance_reducible]

noncomputable instance WeierstrassCurve.FormalGroupPoint.instAddOfFactIsAdic {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] : Add (W.FormalGroupPoint I)

Addition of formal-group points is evaluation of the Weierstrass formal group law.

Equations

• WeierstrassCurve.FormalGroupPoint.instAddOfFactIsAdic = { add := fun (P Q : W.FormalGroupPoint I) => { val := W.formalAddEval P.val Q.val, property := ⋯ } }

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_add {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] (P Q : W.FormalGroupPoint I) : (P + Q).val = W.formalAddEval P.val Q.val

@[instance_reducible]

noncomputable instance WeierstrassCurve.FormalGroupPoint.instNegOfFactIsAdic {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] : Neg (W.FormalGroupPoint I)

Negation of a formal-group point is evaluation of the formal inverse.

Equations

• WeierstrassCurve.FormalGroupPoint.instNegOfFactIsAdic = { neg := fun (P : W.FormalGroupPoint I) => { val := W.formalInverseEval P.val, property := ⋯ } }

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_neg {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] (P : W.FormalGroupPoint I) : (-P).val = W.formalInverseEval P.val

@[instance_reducible]

noncomputable instance WeierstrassCurve.FormalGroupPoint.instAddCommGroup {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] : AddCommGroup (W.FormalGroupPoint I)

The elements of an adic ideal form an additive commutative group under the evaluated Weierstrass formal group law.

Equations

• WeierstrassCurve.FormalGroupPoint.instAddCommGroup = { toAddGroup := AddGroup.ofLeftAxioms ⋯ ⋯ ⋯, add_comm := ⋯ }