The indecomposables of the Lazard ring

The Lazard ring L is augmented over ℤ by the homomorphism η : L →+* ℤ classifying the additive formal group law X + Y; it sends every coefficient aᵢⱼ, i, j ≥ 1, of the nonlinear part of the universal formal group law to 0, and its kernel, the augmentation ideal I, is generated by the aᵢⱼ. The indecomposables of L are the ℤ-module Q(L) = I ⧸ I² (Ideal.Cotangent). This file proves Lazard's computation of the indecomposables: Q(L) is a free ℤ-module with one basis element in each degree 2n, n ≥ 1, the class of an explicit element xₙ ∈ L₂ₙ.

Modulo I² the coefficients of the nonlinear part of the universal formal group law have square zero, so that nonlinear part is a symmetric additive 2-cocycle with coefficients in L ⧸ I² (FormalGroup.isSymmetricCocycleCoeff_coeff). By the symmetric 2-cocycle lemma its homogeneous part of degree n + 1 is a multiple of the Lazard cocycle C_{n+1}, so modulo I² each a_{i, n+1-i} is ((n + 1).choose i / d_{n+1}) • xₙ, where xₙ = ∑ cᵢ a_{i, n+1-i} for integers cᵢ with ∑ cᵢ ((n + 1).choose i / d_{n+1}) = 1, which exist since these numbers are coprime. Conversely, the formal group law X + Y + ε C_{n+1}(X, Y) over the dual numbers ℤ[ε], ε² = 0, is classified by a homomorphism L →+* ℤ[ε] that kills I² and every xₘ with m ≠ n and sends xₙ to ε. Hence the classes of the xₙ are linearly independent.

This is the input to Lazard's theorem that L is a polynomial ring ℤ[x₁, x₂, …]: lifts of a basis of the indecomposables of a connected graded ring generate it.

Main definitions

• TauCeti.LazardRing.augmentation: the augmentation L →+* ℤ, classifying X + Y.
• TauCeti.LazardRing.augmentationIdeal: its kernel I.
• TauCeti.LazardRing.generator n: the element xₙ ∈ L₂ₙ.
• TauCeti.LazardRing.cotangentBasis: the basis (xₙ mod I²)ₙ of Q(L) = I ⧸ I² over ℤ.

Main results

• TauCeti.LazardRing.augmentationIdeal_eq_span: I is generated by the coefficients aᵢⱼ.
• TauCeti.LazardRing.augmentationIdeal_eq_irrelevant: I is the irrelevant ideal ⨁_{n > 0} Lₙ.
• TauCeti.LazardRing.intCast_augmentation_of_mem_grading_zero: L is connected, L₀ = ℤ.
• TauCeti.LazardRing.generator_mem_grading: xₙ has degree 2n.
• TauCeti.LazardRing.coeff_formalGroup_sub_nsmul_generator_mem_sq: for 0 < i ≤ n, a_{i, n+1-i} ≡ ((n + 1).choose i / d_{n+1}) • xₙ modulo I².
• TauCeti.LazardRing.cotangentBasis_apply: the basis vectors are the classes of the xₙ.
• TauCeti.LazardRing.sub_sum_generator_mem_sq: modulo I², an element of I is the combination of the xₙ given by its coordinates in this basis.

References

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

The augmentation

noncomputable def TauCeti.LazardRing.augmentation : LazardRing →+* ℤ

The augmentation L →+* ℤ of the Lazard ring: the homomorphism classifying the additive formal group law X + Y. It sends every coefficient aᵢⱼ, i, j ≥ 1, of the nonlinear part of the universal formal group law to 0.

@[simp]

theorem TauCeti.LazardRing.augmentation_coeff_formalGroup (d : Fin 2 →₀ ℕ) : augmentation ((MvPowerSeries.coeff d) formalGroup.toPowerSeries) = (MvPowerSeries.coeff d) (MvPowerSeries.X 0 + MvPowerSeries.X 1)

The augmentation sends a coefficient of the universal formal group law to the corresponding coefficient of X + Y.

@[simp]

theorem TauCeti.LazardRing.map_augmentation : formalGroup.map augmentation = FormalGroup.𝔾ₐ

The augmentation classifies the additive formal group law.

@[simp]

theorem TauCeti.LazardRing.augmentation_mk (p : MvPolynomial (ℕ+ × ℕ+) ℤ) : augmentation (mk p) = MvPolynomial.constantCoeff p

On polynomials in the aᵢⱼ, the augmentation is the constant coefficient.

noncomputable def TauCeti.LazardRing.augmentationIdeal : Ideal LazardRing

The augmentation ideal I of the Lazard ring, the kernel of the augmentation.

@[simp]

theorem TauCeti.LazardRing.mem_augmentationIdeal {x : LazardRing} : x ∈ augmentationIdeal ↔ augmentation x = 0

An element lies in the augmentation ideal exactly when its augmentation vanishes.

theorem TauCeti.LazardRing.augmentationIdeal_eq_span : augmentationIdeal = Ideal.span (Set.range fun (ij : ℕ+ × ℕ+) => mk (MvPolynomial.X ij))

The augmentation ideal is generated by the coefficients aᵢⱼ of the universal formal group law.

theorem TauCeti.LazardRing.mk_X_mem_augmentationIdeal (ij : ℕ+ × ℕ+) : mk (MvPolynomial.X ij) ∈ augmentationIdeal

The coefficients aᵢⱼ of the universal formal group law lie in the augmentation ideal.

theorem TauCeti.LazardRing.augmentationIdeal_eq_irrelevant : augmentationIdeal = (HomogeneousIdeal.irrelevant grading).toIdeal

The augmentation ideal is the irrelevant ideal ⨁_{n > 0} Lₙ of the grading of the Lazard ring.

theorem TauCeti.LazardRing.intCast_augmentation_of_mem_grading_zero {x : LazardRing} (hx : x ∈ grading 0) : ↑(augmentation x) = x

The Lazard ring is connected: an element of degree 0 is the integer given by its augmentation, so L₀ = ℤ.

theorem TauCeti.LazardRing.coeff_formalGroup_sub_mem_augmentationIdeal (d : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff d) (formalGroup.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) ∈ augmentationIdeal

The coefficients of the nonlinear part F - X - Y of the universal formal group law lie in the augmentation ideal.

The generators

noncomputable def TauCeti.LazardRing.generator (n : ℕ+) : LazardRing

The generator xₙ of the indecomposables of the Lazard ring in degree 2n: the integral combination ∑_{0 < i ≤ n} cᵢ a_{i, n+1-i} of the coefficients of the universal formal group law in total degree n + 1, for integers cᵢ with ∑ cᵢ ((n + 1).choose i / d_{n+1}) = 1. Only its class modulo the square of the augmentation ideal is determined by this property, and that class is the n-th vector of TauCeti.LazardRing.cotangentBasis.

theorem TauCeti.LazardRing.generator_mem_grading (n : ℕ+) : generator n ∈ grading (2 * ↑n)

The generator xₙ has degree 2n.

theorem TauCeti.LazardRing.generator_mem_augmentationIdeal (n : ℕ+) : generator n ∈ augmentationIdeal

The generator xₙ lies in the augmentation ideal.

The indecomposables are generated by the classes of the generators

theorem TauCeti.LazardRing.coeff_formalGroup_sub_nsmul_generator_mem_sq (n : ℕ+) {i : ℕ} (hi : 0 < i) (hin : i ≤ ↑n) : (MvPowerSeries.coeff (Finsupp.single 0 i + Finsupp.single 1 (↑n + 1 - i))) formalGroup.toPowerSeries - ((↑n + 1).choose i / lazardGcd (↑n + 1)) • generator n ∈ augmentationIdeal ^ 2

The coefficients of the universal formal group law modulo decomposables: for 0 < i ≤ n, a_{i, n+1-i} ≡ ((n + 1).choose i / d_{n+1}) • xₙ modulo the square of the augmentation ideal.

Detecting the generators

The basis of the indecomposables

noncomputable def TauCeti.LazardRing.cotangentBasis : Module.Basis ℕ+ ℤ augmentationIdeal.Cotangent

Lazard's computation of the indecomposables of the Lazard ring. The ℤ-module I ⧸ I² of indecomposables of L, for I the augmentation ideal, is free with basis the classes of the generators xₙ ∈ L₂ₙ, n ≥ 1.

@[simp]

theorem TauCeti.LazardRing.cotangentBasis_apply (n : ℕ+) : cotangentBasis n = augmentationIdeal.toCotangent ⟨generator n, ⋯⟩

The n-th vector of the basis of the indecomposables is the class of the generator xₙ.

theorem TauCeti.LazardRing.sub_sum_generator_mem_sq {y : LazardRing} (hy : y ∈ augmentationIdeal) : y - ↑((cotangentBasis.repr (augmentationIdeal.toCotangent ⟨y, hy⟩)).sum fun (n : ℕ+) (k : ℤ) => k • ⟨generator n, ⋯⟩) ∈ augmentationIdeal ^ 2

Modulo the square of the augmentation ideal, an element y of the augmentation ideal is the combination ∑ cₙ xₙ of the generators, where (cₙ)ₙ are the coordinates of the class of y in the basis TauCeti.LazardRing.cotangentBasis of I ⧸ I².