Points of a formal group law in topologically nilpotent elements

Let F(X, Y) be a one-dimensional formal group law over a commutative ring R, and let A be a complete Hausdorff linearly topologised R-algebra. The power series F converges at every pair of topologically nilpotent elements of A, and its value is again topologically nilpotent. So the topologically nilpotent elements of A form a group under x +_F y = F(x, y), with negation the value i(x) of the formal inverse. This is the group F(A) of A-valued points of F; for a complete local ring A with its 𝔪-adic topology it is the maximal ideal 𝔪 with the law F.

The carrier F.TopNilpotentPoint A mirrors Mathlib's power-series carrier F.Point σ of series with nilpotent constant coefficient: a point is an element of A satisfying PowerSeries.HasEval, the condition that makes evaluation converge. Mathlib's carrier is the special case A = R⟦σ⟧ with the product topology over discrete R (FormalGroup.pointEquivTopNilpotentPoint). Evaluation uses the discrete topology on R, so no topology on the coefficient ring is assumed. Characterising lemmas are stated as convergent sums, which mention no topology on R either.

Main definitions

• FormalGroup.TopNilpotentPoint F A: the topologically nilpotent elements of A, carrying an AddGroup structure, and an AddCommGroup structure when F is commutative.
• FormalGroup.TopNilpotentPoint.map: a continuous R-algebra map A → B induces an additive map F(A) → F(B).
• FormalGroup.pointEquivTopNilpotentPoint: the group F.Point σ of power-series points is the group of points of F in R⟦σ⟧.
• FormalGroup.substPointHom: substitution of a family of series into power-series points, as an additive map F.Point σ → F.Point τ.

Main results

• FormalGroup.TopNilpotentPoint.hasSum_val_add: x +_F y is the sum of the convergent series ∑ aᵢⱼ xⁱ yʲ.
• FormalGroup.TopNilpotentPoint.hasSum_val_neg: -x is the sum of the convergent series ∑ cₙ xⁿ, where i(X) = ∑ cₙ Xⁿ is the formal inverse.
• FormalGroup.TopNilpotentPoint.map_id, FormalGroup.TopNilpotentPoint.map_comp: functoriality.
• FormalGroup.substPointHom_X, FormalGroup.substPointHom_comp: functoriality of power-series points along substitutions.

Implementation notes

The group laws are not proved by manipulating the convergent sums. Evaluation at a family of topologically nilpotent elements turns substitution into evaluation (MvPowerSeries.eval₂_subst), so each law in F(A) is the evaluation of the corresponding identity of power series: associativity of F, the unit laws F(X, 0) = X = F(0, X) and F(i(X), X) = 0.

WeierstrassCurve.FormalGroupPoint is the same construction for the formal group law of a Weierstrass curve, which is not a FormalGroup, on an adic ideal.

References

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

structure FormalGroup.TopNilpotentPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) (A : Type u_2) [CommRing A] [TopologicalSpace A] : Type u_2

The points of a formal group law F in A: the elements of a topological ring A satisfying PowerSeries.HasEval, that is, the topologically nilpotent elements. Evaluation of power series over R at these elements converges when A is a complete, Hausdorff, linearly topologised R-algebra; under those assumptions they form a group under x +_F y = F(x, y). This is the analogue for A of the power-series carrier F.Point σ.

This is a structure rather than a subtype of A so that its group law, which depends on F, is not confused with the ring operations of A.

• val : A

  The coordinate of a point.

• hasEval : PowerSeries.HasEval self.val

  The coordinate of a point is topologically nilpotent.

theorem FormalGroup.TopNilpotentPoint.ext {R : Type u_1} {inst✝ : CommRing R} {F : FormalGroup R} {A : Type u_2} {inst✝¹ : CommRing A} {inst✝² : TopologicalSpace A} {x y : F.TopNilpotentPoint A} (val : x.val = y.val) : x = y

theorem FormalGroup.TopNilpotentPoint.ext_iff {R : Type u_1} {inst✝ : CommRing R} {F : FormalGroup R} {A : Type u_2} {inst✝¹ : CommRing A} {inst✝² : TopologicalSpace A} {x y : F.TopNilpotentPoint A} : x = y ↔ x.val = y.val

@[instance_reducible]

instance FormalGroup.TopNilpotentPoint.instZero {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [TopologicalSpace A] : Zero (F.TopNilpotentPoint A)

The zero point.

@[simp]

theorem FormalGroup.TopNilpotentPoint.val_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [TopologicalSpace A] : val 0 = 0

@[instance_reducible]

noncomputable instance FormalGroup.TopNilpotentPoint.instAdd {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] : Add (F.TopNilpotentPoint A)

The sum x +_F y = F(x, y) of two points.

@[instance_reducible]

noncomputable instance FormalGroup.TopNilpotentPoint.instNeg {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] : Neg (F.TopNilpotentPoint A)

The negation -x = i(x) of a point, the value of the formal inverse.

theorem FormalGroup.TopNilpotentPoint.val_add_eq_eval₂ {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] [UniformSpace R] [DiscreteUniformity R] (x y : F.TopNilpotentPoint A) : (x + y).val = MvPowerSeries.eval₂ (algebraMap R A) ![x.val, y.val] F.toPowerSeries

The sum of two points as an evaluation, for any discrete uniform structure on R.

theorem FormalGroup.TopNilpotentPoint.val_neg_eq_eval₂ {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] [UniformSpace R] [DiscreteUniformity R] (x : F.TopNilpotentPoint A) : (-x).val = PowerSeries.eval₂ (algebraMap R A) x.val F.addInvX

The negation of a point as an evaluation, for any discrete uniform structure on R.

theorem FormalGroup.TopNilpotentPoint.hasSum_val_add {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] (x y : F.TopNilpotentPoint A) : HasSum (fun (d : Fin 2 →₀ ℕ) => (MvPowerSeries.coeff d) F.toPowerSeries • (x.val ^ d 0 * y.val ^ d 1)) (x + y).val

The sum of two points is a convergent series: x +_F y = ∑ aᵢⱼ xⁱ yʲ, where F(X, Y) = ∑ aᵢⱼ Xⁱ Yʲ.

theorem FormalGroup.TopNilpotentPoint.hasSum_val_neg {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] (x : F.TopNilpotentPoint A) : HasSum (fun (n : ℕ) => (PowerSeries.coeff n) F.addInvX • x.val ^ n) (-x).val

The negation of a point is a convergent series: -x = ∑ cₙ xⁿ, where i(X) = ∑ cₙ Xⁿ is the formal inverse of F.

theorem FormalGroup.TopNilpotentPoint.val_add_eq_tsum {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] (x y : F.TopNilpotentPoint A) : (x + y).val = ∑' (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries • (x.val ^ d 0 * y.val ^ d 1)

The sum of two points is ∑ aᵢⱼ xⁱ yʲ, where F(X, Y) = ∑ aᵢⱼ Xⁱ Yʲ.

theorem FormalGroup.TopNilpotentPoint.val_neg_eq_tsum {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] (x : F.TopNilpotentPoint A) : (-x).val = ∑' (n : ℕ), (PowerSeries.coeff n) F.addInvX • x.val ^ n

The negation of a point is ∑ cₙ xⁿ, where i(X) = ∑ cₙ Xⁿ is the formal inverse.

@[instance_reducible]

noncomputable instance FormalGroup.TopNilpotentPoint.instAddGroup {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] : AddGroup (F.TopNilpotentPoint A)

The points of F in A form a group under x +_F y = F(x, y), with -x = i(x). Each law is the evaluation of the corresponding identity of power series.

@[instance_reducible]

noncomputable instance FormalGroup.TopNilpotentPoint.instAddCommGroupOfIsComm {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] [F.IsComm] : AddCommGroup (F.TopNilpotentPoint A)

The points of a commutative formal group law form a commutative group.

noncomputable def FormalGroup.TopNilpotentPoint.map {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] {B : Type u_3} [CommRing B] [Algebra R B] [UniformSpace B] [IsUniformAddGroup B] [CompleteSpace B] [T2Space B] [IsTopologicalRing B] [IsLinearTopology B B] (φ : A →A[R] B) : F.TopNilpotentPoint A →+ F.TopNilpotentPoint B

A continuous R-algebra map φ : A → B maps points of F in A to points of F in B, additively: φ(F(x, y)) = F(φ(x), φ(y)).

@[simp]

theorem FormalGroup.TopNilpotentPoint.val_map {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] {B : Type u_3} [CommRing B] [Algebra R B] [UniformSpace B] [IsUniformAddGroup B] [CompleteSpace B] [T2Space B] [IsTopologicalRing B] [IsLinearTopology B B] (φ : A →A[R] B) (x : F.TopNilpotentPoint A) : ((map F φ) x).val = φ x.val

@[simp]

theorem FormalGroup.TopNilpotentPoint.map_id {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] : map F (ContinuousAlgHom.id R A) = AddMonoidHom.id (F.TopNilpotentPoint A)

theorem FormalGroup.TopNilpotentPoint.map_comp {R : Type u_1} [CommRing R] (F : FormalGroup R) {A : Type u_2} [CommRing A] [Algebra R A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsLinearTopology A A] {B : Type u_3} {C : Type u_4} [CommRing B] [Algebra R B] [UniformSpace B] [IsUniformAddGroup B] [CompleteSpace B] [T2Space B] [IsTopologicalRing B] [IsLinearTopology B B] [CommRing C] [Algebra R C] [UniformSpace C] [IsUniformAddGroup C] [CompleteSpace C] [T2Space C] [IsTopologicalRing C] [IsLinearTopology C C] (ψ : B →A[R] C) (φ : A →A[R] B) : map F (ψ.comp φ) = (map F ψ).comp (map F φ)

noncomputable def FormalGroup.pointEquivTopNilpotentPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) [UniformSpace R] [DiscreteUniformity R] (σ : Type u_2) : F.Point σ ≃+ F.TopNilpotentPoint (MvPowerSeries σ R)

Power-series points are points in R⟦σ⟧. The group F.Point σ of power series with nilpotent constant coefficient, under substitution into F, is the group of points of F in R⟦σ⟧ with the product topology over discrete R: a power series is topologically nilpotent exactly when its constant coefficient is nilpotent, and substitution is evaluation.

@[simp]

theorem FormalGroup.val_pointEquivTopNilpotentPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) [UniformSpace R] [DiscreteUniformity R] (σ : Type u_2) (x : F.Point σ) : ((F.pointEquivTopNilpotentPoint σ) x).val = ↑x

@[simp]

theorem FormalGroup.val_pointEquivTopNilpotentPoint_symm {R : Type u_1} [CommRing R] (F : FormalGroup R) [UniformSpace R] [DiscreteUniformity R] (σ : Type u_2) (x : F.TopNilpotentPoint (MvPowerSeries σ R)) : ↑((F.pointEquivTopNilpotentPoint σ).symm x) = x.val

noncomputable def FormalGroup.substPointHom {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_2} {τ : Type u_3} {a : σ → MvPowerSeries τ R} (ha : MvPowerSeries.HasSubst a) : F.Point σ →+ F.Point τ

Power-series points are functorial along substitutions. Substituting a family a of series into the power-series points of F is additive. It is the map of points (FormalGroup.TopNilpotentPoint.map) induced by the continuous R-algebra map subst a : R⟦σ⟧ → R⟦τ⟧, read through FormalGroup.pointEquivTopNilpotentPoint; the product topology over discrete R is used only in this construction.

@[simp]

theorem FormalGroup.val_substPointHom {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_2} {τ : Type u_3} {a : σ → MvPowerSeries τ R} (ha : MvPowerSeries.HasSubst a) (x : F.Point σ) : ↑((F.substPointHom ha) x) = MvPowerSeries.subst a ↑x

@[simp]

theorem FormalGroup.substPointHom_X {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_2} : F.substPointHom ⋯ = AddMonoidHom.id (F.Point σ)

Substituting the variables themselves is the identity on points.

theorem FormalGroup.substPointHom_comp {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_2} {τ : Type u_3} {υ : Type u_4} {a : σ → MvPowerSeries τ R} {b : τ → MvPowerSeries υ R} (ha : MvPowerSeries.HasSubst a) (hb : MvPowerSeries.HasSubst b) : (F.substPointHom hb).comp (F.substPointHom ha) = F.substPointHom ⋯

Substituting a and then b into points is substituting the composite family.