The generators of the Lazard ring are algebraically independent

The generators xₙ ∈ L₂ₙ of the indecomposables of the Lazard ring L (TauCeti.LazardRing.generator) are algebraically independent over ℤ: the homomorphism ℤ[x₁, x₂, …] → L sending xₙ to the generator xₙ is injective. This is the integral independence half of Lazard's theorem that L is the polynomial ring ℤ[x₁, x₂, …].

The proof maps L to ℤ[b₁, b₂, …] by the Hurewicz homomorphism TauCeti.LazardRing.hurewicz, which classifies the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1). Giving bᵢ the degree 2i, it is graded, and the image of xₙ has coefficient d_{n+1} ≠ 0 at bₙ (TauCeti.LazardRing.coeff_single_hurewicz_generator).

A polynomial of degree 2n is a combination of bₙ and of monomials in b₁, …, bₙ₋₁, so for the lexicographic order in which variables of larger index are more significant the leading monomial of the image of xₙ is bₙ. Polynomials with distinct leading variables are algebraically independent (MonomialOrder.algebraicIndependent_of_degree_eq_single), hence so are the images of the xₙ, and the xₙ themselves.

Main results

• TauCeti.LazardRing.algebraicIndependent_hurewicz_generator: the images of the generators xₙ under the Hurewicz homomorphism are algebraically independent over ℤ.
• TauCeti.LazardRing.algebraicIndependent_generator: the generators xₙ of the Lazard ring are algebraically independent over ℤ.

References

• M. Lazard, Sur les groupes de Lie formels à un paramètre, Bull. Soc. Math. France 83 (1955).
• J. F. Adams, Stable Homotopy and Generalised Homology, Part II, §7.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1 (Lazard's theorem A2.1.8).

The leading monomial of ρ(xₙ)

theorem TauCeti.LazardRing.algebraicIndependent_hurewicz_generator : AlgebraicIndependent ℤ (⇑hurewicz ∘ generator)

The images hurewicz xₙ ∈ ℤ[b₁, b₂, …] of the generators of the Lazard ring are algebraically independent over ℤ.

theorem TauCeti.LazardRing.algebraicIndependent_generator : AlgebraicIndependent ℤ generator

Lazard's theorem, integral independence: the generators xₙ ∈ L₂ₙ of the Lazard ring are algebraically independent over ℤ, that is, the homomorphism ℤ[x₁, x₂, …] → L sending xₙ to TauCeti.LazardRing.generator n is injective.