Additive power series

A power series h(X) over a commutative ring R is additive if h(X + Y) = h(X) + h(Y) in R⟦X, Y⟧, that is, if it is an endomorphism of the additive formal group law X + Y. Writing h = ∑ cₙ Xⁿ, the coefficient of XⁱYʲ in h(X + Y) is (i + j).choose i * c_{i+j}, so h is additive exactly when c₀ = 0 and n.choose i * cₙ = 0 for all 0 < i < n.

For instance, over a ℚ-algebra the additive series are the multiples c₁ X. If p = 0 in R for a prime p, the binomial coefficients n.choose i, 0 < i < n, of n ≥ 1 are all divisible by p exactly when n is a power of p, and an integer prime to p is a unit in R. So in that case h is additive exactly when its coefficients vanish away from the powers of p:

h = ∑_{k ≥ 0} b_k X^(p ^ k), b_k = c_{p ^ k}.

This coefficient description needs no other hypothesis on R: it may be the zero ring or have nilpotents. If R is moreover Hausdorff, the displayed sum is a convergent sum for the coefficientwise topology, and the additive series are exactly the sums of this form.

For p = 2 this describes the freedom in the strict logarithm g(X) = X + ⋯ of a commutative formal group law F with [2]_F = 0, which satisfies g(F(X, Y)) = g(X) + g(Y): composing g with an additive series h with c₁ = 1 gives another one, h(g(F(X, Y))) = h(g(X)) + h(g(Y)) by PowerSeries.subst_add_of_subst_X_add_X_eq_add.

Main results

• PowerSeries.coeff_subst_X_add_X: the coefficient of XⁱYʲ in h(X + Y) is (i + j).choose i * c_{i+j}.
• PowerSeries.subst_X_add_X_eq_add_iff: h(X + Y) = h(X) + h(Y) exactly when c₀ = 0 and n.choose i * cₙ = 0 for 0 < i < n.
• PowerSeries.subst_add_of_subst_X_add_X_eq_add: an additive series satisfies h(a + b) = h(a) + h(b) for all power series a, b that can be substituted.
• PowerSeries.subst_X_add_X_eq_add_iff_of_natCast_eq_zero: if p = 0 in R for a prime p, h is additive exactly when cₙ = 0 unless n is a power of p.
• PowerSeries.WithPiTopology.subst_X_add_X_eq_add_iff_exists_hasSum: if p = 0 in R and R is Hausdorff, h is additive exactly when h = ∑_k b_k X^(p ^ k) for some b : ℕ → R.

References

• M. Hazewinkel, Formal Groups and Applications, I §1.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.

theorem PowerSeries.coeff_subst_X_add_X {R : Type u_1} [CommRing R] (h : PowerSeries R) (i j : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 i + Finsupp.single 1 j)) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h) = ↑((i + j).choose i) * (coeff (i + j)) h

The coefficient of XⁱYʲ in h(X + Y) is (i + j).choose i times the coefficient of X^(i + j) in h.

theorem PowerSeries.subst_X_add_X_eq_add_iff {R : Type u_1} [CommRing R] (h : PowerSeries R) : subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h = subst (MvPowerSeries.X 0) h + subst (MvPowerSeries.X 1) h ↔ constantCoeff h = 0 ∧ ∀ (n i : ℕ), 0 < i → i < n → ↑(n.choose i) * (coeff n) h = 0

The additive power series. A power series h satisfies h(X + Y) = h(X) + h(Y) exactly when its constant coefficient vanishes and n.choose i kills its coefficient of Xⁿ for every 0 < i < n.

theorem PowerSeries.subst_add_of_subst_X_add_X_eq_add {R : Type u_1} [CommRing R] {h : PowerSeries R} (hh : subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h = subst (MvPowerSeries.X 0) h + subst (MvPowerSeries.X 1) h) {σ : Type u_2} {a b : MvPowerSeries σ R} (ha : HasSubst a) (hb : HasSubst b) : subst (a + b) h = subst a h + subst b h

An additive power series h satisfies h(a + b) = h(a) + h(b) for all power series a, b in any number of variables that can be substituted into h.

theorem PowerSeries.subst_X_add_X_eq_add_iff_of_natCast_eq_zero {R : Type u_1} [CommRing R] {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) (h : PowerSeries R) : subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h = subst (MvPowerSeries.X 0) h + subst (MvPowerSeries.X 1) h ↔ ∀ (n : ℕ), (∀ (k : ℕ), n ≠ p ^ k) → (coeff n) h = 0

The additive power series when p = 0. If p = 0 in R for a prime p, a power series h satisfies h(X + Y) = h(X) + h(Y) exactly when its coefficient of Xⁿ vanishes for every n that is not a power of p; that is, h = ∑_k b_k X^(p ^ k).

theorem PowerSeries.WithPiTopology.hasSum_monomial_prime_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) {h : PowerSeries R} (hh : subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h = subst (MvPowerSeries.X 0) h + subst (MvPowerSeries.X 1) h) : HasSum (fun (k : ℕ) => (monomial (p ^ k)) ((coeff (p ^ k)) h)) h

If p = 0 in R for a prime p, an additive power series h is the sum ∑_k c_{p ^ k} X^(p ^ k) of its monomials in the degrees p ^ k.

theorem PowerSeries.WithPiTopology.subst_X_add_X_eq_add_iff_exists_hasSum {R : Type u_1} [CommRing R] [TopologicalSpace R] [T2Space R] {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) (h : PowerSeries R) : subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) h = subst (MvPowerSeries.X 0) h + subst (MvPowerSeries.X 1) h ↔ ∃ (b : ℕ → R), HasSum (fun (k : ℕ) => (monomial (p ^ k)) (b k)) h

The additive power series when p = 0, as sums. If p = 0 in R for a prime p and R is Hausdorff, a power series h satisfies h(X + Y) = h(X) + h(Y) exactly when h = ∑_k b_k X^(p ^ k) for some coefficients b : ℕ → R, the sum converging coefficientwise.