Lazard's theorem: the Lazard ring is a polynomial ring

The Lazard ring L is the polynomial ring ℤ[x₁, x₂, …] on the generators xₙ = TauCeti.LazardRing.generator n of degree 2n.

The generators are algebraically independent (TauCeti.LazardRing.algebraicIndependent_generator). They also generate L as a ring: L is connected (L₀ = ℤ), its augmentation ideal I is the irrelevant ideal ⨁_{n > 0} Lₙ, and the classes of the xₙ form a basis of the indecomposables I ⧸ I² (TauCeti.LazardRing.cotangentBasis). By the graded Nakayama lemma (TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le), homogeneous elements of positive degree whose classes generate I ⧸ I² generate L over L₀ = ℤ.

The resulting isomorphism ℤ[x₁, x₂, …] ≃ₐ[ℤ] L is graded when xₙ is given degree 2n.

Since L is a polynomial ring, ring homomorphisms out of L lift along surjective ring homomorphisms (MvPolynomial.exists_comp_eq_of_surjective). By the universal property of L, every commutative formal group law over S is therefore the base change of a commutative formal group law over R along any surjection R →+* S. This is the use Lubin and Tate make of Lazard's theorem: commutative formal group laws over A ⧸ I lift to A, so deformations of a commutative formal group law exist over every ring surjecting onto its coefficient ring.

Main definitions

• TauCeti.LazardRing.mvPolynomialEquiv: the isomorphism ℤ[x₁, x₂, …] ≃ₐ[ℤ] L sending xₙ to the generator xₙ.

Main results

• TauCeti.LazardRing.adjoin_range_generator: the generators xₙ generate L as a ring.
• TauCeti.LazardRing.hurewicz_injective: the Hurewicz homomorphism L →+* ℤ[b₁, b₂, …] is injective.
• TauCeti.LazardRing.mvPolynomialEquiv_mem_grading_iff: the isomorphism carries the polynomials that are homogeneous of degree n, for xₖ of degree 2k, onto Lₙ.
• TauCeti.LazardRing.exists_comp_eq_of_surjective: a ring homomorphism L →+* S factors through any surjective ring homomorphism R →+* S.
• FormalGroup.exists_map_eq_of_surjective: a commutative formal group law over S is the base change of a commutative formal group law over R along any surjective R →+* S.

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).
• J. Lubin and J. Tate, Formal moduli for one-parameter formal Lie groups, Bull. Soc. Math. France 94 (1966).

theorem TauCeti.LazardRing.adjoin_range_generator : Algebra.adjoin ℤ (Set.range generator) = ⊤

Lazard's theorem, generation: the generators xₙ ∈ L₂ₙ generate the Lazard ring as a ring.

noncomputable def TauCeti.LazardRing.mvPolynomialEquiv : MvPolynomial ℕ+ ℤ ≃ₐ[ℤ] LazardRing

Lazard's theorem: the Lazard ring is the polynomial ring ℤ[x₁, x₂, …] on the generators xₙ = TauCeti.LazardRing.generator n. The isomorphism is evaluation at the generators.

theorem TauCeti.LazardRing.mvPolynomialEquiv_apply (p : MvPolynomial ℕ+ ℤ) : mvPolynomialEquiv p = (MvPolynomial.aeval generator) p

The isomorphism ℤ[x₁, x₂, …] ≃ₐ[ℤ] L is evaluation at the generators.

@[simp]

theorem TauCeti.LazardRing.mvPolynomialEquiv_X (n : ℕ+) : mvPolynomialEquiv (MvPolynomial.X n) = generator n

The isomorphism ℤ[x₁, x₂, …] ≃ₐ[ℤ] L sends the variable xₙ to the generator xₙ.

@[simp]

theorem TauCeti.LazardRing.mvPolynomialEquiv_symm_generator (n : ℕ+) : mvPolynomialEquiv.symm (generator n) = MvPolynomial.X n

The inverse isomorphism L ≃ₐ[ℤ] ℤ[x₁, x₂, …] sends the generator xₙ to the variable xₙ.

theorem TauCeti.LazardRing.hurewicz_injective : Function.Injective ⇑hurewicz

The Hurewicz homomorphism of the Lazard ring is injective: the homomorphism L →+* ℤ[b₁, b₂, …] classifying the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1) embeds L in ℤ[b₁, b₂, …].

theorem TauCeti.LazardRing.mvPolynomialEquiv_mem_grading_iff {p : MvPolynomial ℕ+ ℤ} {n : ℕ} : mvPolynomialEquiv p ∈ grading n ↔ MvPolynomial.IsWeightedHomogeneous (fun (k : ℕ+) => 2 * ↑k) p n

Lazard's theorem, graded: giving the variable xₖ the degree 2k, the isomorphism ℤ[x₁, x₂, …] ≃ₐ[ℤ] L carries the polynomials that are homogeneous of degree n exactly onto the degree-n part Lₙ of the Lazard ring.

theorem TauCeti.LazardRing.exists_comp_eq_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) (g : LazardRing →+* S) : ∃ (g' : LazardRing →+* R), f.comp g' = g

Ring homomorphisms out of the Lazard ring lift along surjective ring homomorphisms: every g : L →+* S factors as f.comp g' through any surjection f : R →+* S.

theorem FormalGroup.exists_map_eq_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup S) [F.IsComm] {f : R →+* S} (hf : Function.Surjective ⇑f) : ∃ (G : FormalGroup R), G.IsComm ∧ G.map f = F

Commutative formal group laws lift along surjections: if f : R →+* S is surjective, every commutative formal group law over S is the base change along f of a commutative formal group law over R.