Coefficients of formal group laws

Mathlib states commutativity of a formal group law F(X, Y) as the identity F(X, Y) = F(Y, X) of power series. This file records its coefficientwise form: the coefficient of XⁱYʲ in F equals that of XʲYⁱ. It also records the lowest-order effect of perturbing an argument of a formal group law: since F(X, Y) = X + Y + ⋯, perturbing x or y by a series e of order at least n ≥ 1 adds e to F(x, y), up to terms of degree greater than n.

Main results

• FormalGroup.coeff_comm: the coefficients of a commutative formal group law are symmetric.
• FormalGroup.le_order_subst_add_left_sub, FormalGroup.le_order_subst_add_right_sub: F(x + e, y) ≡ F(x, y) + e and F(x, y + e) ≡ F(x, y) + e modulo terms of degree greater than n, for e of order at least n ≥ 1.

theorem FormalGroup.coeff_comm {A : Type u_1} [CommRing A] (F : FormalGroup A) [F.IsComm] (i j : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 i + Finsupp.single 1 j)) F.toPowerSeries = (MvPowerSeries.coeff (Finsupp.single 0 j + Finsupp.single 1 i)) F.toPowerSeries

The coefficients of a commutative formal group law are symmetric: the coefficient of XⁱYʲ equals that of XʲYⁱ.

theorem FormalGroup.le_order_subst_add_left_sub {A : Type u_1} [CommRing A] (F : FormalGroup A) {σ : Type u_2} {x y e : MvPowerSeries σ A} (hx : MvPowerSeries.constantCoeff x = 0) (hy : MvPowerSeries.constantCoeff y = 0) {n : ℕ} (hn : n ≠ 0) (he : ↑n ≤ e.order) : ↑(n + 1) ≤ (MvPowerSeries.subst ![x + e, y] F.toPowerSeries - MvPowerSeries.subst ![x, y] F.toPowerSeries - e).order

Perturbing the first argument of F by a series e of order at least n ≥ 1 adds e to F(x, y), up to terms of degree greater than n.

theorem FormalGroup.le_order_subst_add_right_sub {A : Type u_1} [CommRing A] (F : FormalGroup A) {σ : Type u_2} {x y e : MvPowerSeries σ A} (hx : MvPowerSeries.constantCoeff x = 0) (hy : MvPowerSeries.constantCoeff y = 0) {n : ℕ} (hn : n ≠ 0) (he : ↑n ≤ e.order) : ↑(n + 1) ≤ (MvPowerSeries.subst ![x, y + e] F.toPowerSeries - MvPowerSeries.subst ![x, y] F.toPowerSeries - e).order

Perturbing the second argument of F by a series e of order at least n ≥ 1 adds e to F(x, y), up to terms of degree greater than n.