The logarithm of a formal group law of exponent two

Let F be a commutative formal group law over a commutative ring R with [2]_F(X) = F(X, X) = 0. Then 2 = 0 in R, since 2 is the linear coefficient of [2]_F, so no logarithm in the sense of FormalGroup.log is available. Nevertheless F is strictly isomorphic to the additive formal group law, and there is a canonical choice of isomorphism: there is a unique power series

g(X) = X + ∑_{i ≥ 2} aᵢ Xⁱ with a_{2ᵏ} = 0 for every k ≥ 1

such that g(F(X, Y)) = g(X) + g(Y). This is the case p = 2 of FormalGroup.existsUnique_logarithm_of_nsmulSeries_eq_zero. Formal group laws with [2]_F = 0 arise in Quillen's description of unoriented bordism, where g is the canonical coordinate; this file names it and records its characterising properties. No coefficient field and no further hypothesis on R is used: it may have nilpotents or be the zero ring.

Main definitions

• FormalGroup.exponentTwoLog: the normalised logarithm g of a commutative formal group law F with [2]_F = 0.

Main results

• FormalGroup.subst_toPowerSeries_exponentTwoLog: g(F(X, Y)) = g(X) + g(Y), and FormalGroup.subst_subst_toPowerSeries_exponentTwoLog: g(F(x, y)) = g(x) + g(y) for substitutable x, y.
• FormalGroup.eq_exponentTwoLog: the normalised logarithm is the unique series g = X + ⋯ without terms of degree 2ᵏ, k ≥ 1, that is additive along F.

References

• D. Quillen, On the formal group laws of unoriented and complex cobordism theory, Bull. Amer. Math. Soc. 75 (1969).
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.

noncomputable def FormalGroup.exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) : PowerSeries R

The normalised logarithm of a formal group law of exponent two (Quillen). For a commutative formal group law F with [2]_F = 0, this is the unique power series g(X) = X + ∑_{i ≥ 2} aᵢ Xⁱ with a_{2ᵏ} = 0 for every k ≥ 1 such that g(F(X, Y)) = g(X) + g(Y); see FormalGroup.eq_exponentTwoLog.

@[simp]

theorem FormalGroup.constantCoeff_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) : PowerSeries.constantCoeff (F.exponentTwoLog hF) = 0

The normalised logarithm has no constant term.

@[simp]

theorem FormalGroup.coeff_one_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) : (PowerSeries.coeff 1) (F.exponentTwoLog hF) = 1

The normalised logarithm has linear coefficient 1.

theorem FormalGroup.coeff_two_pow_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) {k : ℕ} (hk : 0 < k) : (PowerSeries.coeff (2 ^ k)) (F.exponentTwoLog hF) = 0

The normalised logarithm has no term of degree 2ᵏ for k ≥ 1.

theorem FormalGroup.subst_toPowerSeries_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) : PowerSeries.subst F.toPowerSeries (F.exponentTwoLog hF) = PowerSeries.subst (MvPowerSeries.X 0) (F.exponentTwoLog hF) + PowerSeries.subst (MvPowerSeries.X 1) (F.exponentTwoLog hF)

The normalised logarithm is additive along F: g(F(X, Y)) = g(X) + g(Y).

theorem FormalGroup.subst_subst_toPowerSeries_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) {σ : Type u_2} {f₀ f₁ : MvPowerSeries σ R} (h₀ : PowerSeries.HasSubst f₀) (h₁ : PowerSeries.HasSubst f₁) : PowerSeries.subst (MvPowerSeries.subst ![f₀, f₁] F.toPowerSeries) (F.exponentTwoLog hF) = PowerSeries.subst f₀ (F.exponentTwoLog hF) + PowerSeries.subst f₁ (F.exponentTwoLog hF)

The normalised logarithm is additive along F at any pair of power series f₀, f₁ that can be substituted: g(F(f₀, f₁)) = g(f₀) + g(f₁).

theorem FormalGroup.eq_exponentTwoLog {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (hF : F.nsmulSeries 2 = 0) {g : PowerSeries R} (h₀ : PowerSeries.constantCoeff g = 0) (h₁ : (PowerSeries.coeff 1) g = 1) (hp : ∀ (k : ℕ), 0 < k → (PowerSeries.coeff (2 ^ k)) g = 0) (hg : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g) : g = F.exponentTwoLog hF

A power series g = X + ⋯ without terms of degree 2ᵏ, k ≥ 1, that is additive along F is the normalised logarithm.