The order filtration on the points of a formal group law

Let G be a formal group law over a commutative ring R. The power-series points G.Point σ vanishing to order N form a subgroup, and when N ≥ 1 the group law of G is ordinary addition on it up to terms of degree above N, since G(X, Y) = X + Y up to terms of degree two divisible by X. So the degree-N part is additive on the points vanishing to order N: this is how identities in the group G.Point σ pass to identities between leading terms.

Main results

• FormalGroup.le_order_subst_sub_sub: if w vanishes to order N ≥ 1 and v has no constant term, then G(w, v) - w - v vanishes to order N + 1.
• FormalGroup.le_order_val_add, FormalGroup.le_order_val_neg, FormalGroup.le_order_val_sub, FormalGroup.le_order_val_sum: the points vanishing to order N form a subgroup.
• FormalGroup.homogeneousComponent_val_add, FormalGroup.homogeneousComponent_val_sub, FormalGroup.homogeneousComponent_val_sum: on points vanishing to order N ≥ 1, the group law of G agrees with ordinary addition in degree N.

theorem FormalGroup.le_order_subst_sub_sub {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ} (hN : N ≠ 0) {w v : MvPowerSeries σ R} (hw : ↑N ≤ w.order) (hv : MvPowerSeries.constantCoeff v = 0) : ↑(N + 1) ≤ (MvPowerSeries.subst ![w, v] G.toPowerSeries - w - v).order

A formal group law is additive to first order. If w vanishes to order N ≥ 1 and v has no constant term, then G(w, v) - w - v vanishes to order N + 1: the monomials of G(X, Y) - X - Y have degree at least two and are divisible by X, since G(0, Y) = Y.

theorem FormalGroup.constantCoeff_val_add {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {x y : G.Point σ} (hx : MvPowerSeries.constantCoeff ↑x = 0) (hy : MvPowerSeries.constantCoeff ↑y = 0) : MvPowerSeries.constantCoeff ↑(x + y) = 0

Sums of points without constant term have no constant term.

theorem FormalGroup.le_order_val_add {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ∞} {x y : G.Point σ} (hx : N ≤ (↑x).order) (hy : N ≤ (↑y).order) : N ≤ (↑(x + y)).order

The points of G vanishing to order N are closed under addition.

theorem FormalGroup.le_order_val_neg {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ∞} {x : G.Point σ} (hx : N ≤ (↑x).order) : N ≤ (↑(-x)).order

The points of G vanishing to order N are closed under negation.

theorem FormalGroup.le_order_val_sub {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ∞} {x y : G.Point σ} (hx : N ≤ (↑x).order) (hy : N ≤ (↑y).order) : N ≤ (↑(x - y)).order

The points of G vanishing to order N are closed under subtraction.

theorem FormalGroup.le_order_val_sum {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} [G.IsComm] {N : ℕ∞} {ι : Type u_3} (s : Finset ι) (t : ι → G.Point σ) (ht : ∀ j ∈ s, N ≤ (↑(t j)).order) : N ≤ (↑(∑ j ∈ s, t j)).order

The points of a commutative formal group law vanishing to order N are closed under finite sums.

theorem FormalGroup.le_order_val_sub_val_sub {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ} (hN : N ≠ 0) {x y : G.Point σ} (hy : MvPowerSeries.constantCoeff ↑y = 0) (h : ↑N ≤ (↑(x - y)).order) : ↑(N + 1) ≤ (↑x - ↑y - ↑(x - y)).order

If x - y vanishes to order N ≥ 1 in the points of G and y has no constant term, then subtraction in G agrees with ordinary subtraction up to degree N + 1.

theorem FormalGroup.homogeneousComponent_val_sub {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ} (hN : N ≠ 0) {x y : G.Point σ} (hy : MvPowerSeries.constantCoeff ↑y = 0) (h : ↑N ≤ (↑(x - y)).order) : (MvPowerSeries.homogeneousComponent N) ↑(x - y) = (MvPowerSeries.homogeneousComponent N) (↑x - ↑y)

If y has no constant term and the difference x - y in G vanishes to order N ≥ 1, the degree-N part of the difference in G is the degree-N part of the ordinary difference.

theorem FormalGroup.homogeneousComponent_val_add {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ} (hN : N ≠ 0) {x y : G.Point σ} (hx : ↑N ≤ (↑x).order) (hy : MvPowerSeries.constantCoeff ↑y = 0) : (MvPowerSeries.homogeneousComponent N) ↑(x + y) = (MvPowerSeries.homogeneousComponent N) ↑x + (MvPowerSeries.homogeneousComponent N) ↑y

If x vanishes to order N ≥ 1 and y has no constant term, the degree-N part of the sum x + y in G is the sum of the degree-N parts.

theorem FormalGroup.homogeneousComponent_val_sum {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} [G.IsComm] {N : ℕ} (hN : N ≠ 0) {ι : Type u_3} (s : Finset ι) (t : ι → G.Point σ) (ht : ∀ j ∈ s, ↑N ≤ (↑(t j)).order) : (MvPowerSeries.homogeneousComponent N) ↑(∑ j ∈ s, t j) = ∑ j ∈ s, (MvPowerSeries.homogeneousComponent N) ↑(t j)

On points of a commutative formal group law vanishing to order N ≥ 1, the degree-N part of a finite sum in G is the sum of the degree-N parts.

theorem FormalGroup.le_order_val_sub_of_le_order_sub {R : Type u_1} [CommRing R] (G : FormalGroup R) {σ : Type u_2} {N : ℕ} {x y : G.Point σ} (hx : MvPowerSeries.constantCoeff ↑x = 0) (hy : MvPowerSeries.constantCoeff ↑y = 0) (h : ↑N ≤ (↑x - ↑y).order) : ↑N ≤ (↑(x - y)).order

If x and y have no constant term and x - y vanishes to order N as power series, then the difference x - y in the points of G vanishes to order N too.