The Hurewicz homomorphism of the Lazard ring

Let f(X) = X + ∑_{i ≥ 1} bᵢ X^(i + 1) be the universal strict coordinate over the polynomial ring ℤ[b₁, b₂, …]. Transporting the additive formal group law along f gives the commutative formal group law f(f⁻¹(X) + f⁻¹(Y)), whose exponential is f. The Hurewicz homomorphism TauCeti.LazardRing.hurewicz : L →+* ℤ[b₁, b₂, …] is the homomorphism classifying this law. It is the reduction ℤ ⊗_L L[b₁, b₂, …] of the right unit of the Hopf algebroid (L, L[b₁, b₂, …]) along the augmentation (TauCeti.LazardRing.map_augmentation_comp_rightUnit). Through Quillen's theorem it corresponds to the Hurewicz homomorphism MU_* → H_*(MU) = ℤ[b₁, b₂, …], and the coefficient of bₙ in the image of an element of MU_{2n} is, up to sign, its characteristic number sₙ.

Giving bᵢ the degree 2i, the Hurewicz homomorphism is graded (TauCeti.LazardRing.isWeightedHomogeneous_hurewicz): conjugating f by the homothety X ↦ 2 X multiplies bᵢ by 2ⁱ and rescales the transported law by 2 (FormalGroup.isWeightedHomogeneous_coeff_ofStrictCoeffs_X_smul_𝔾ₐ).

The linear coefficients of the Hurewicz homomorphism compute the indecomposables of L. The coefficient of bₙ kills the square of the augmentation ideal I; evaluating at bₙ = ε, ε² = 0, turns the transported law into X + Y + ε ((X + Y)^(n + 1) - X^(n + 1) - Y^(n + 1)), whose coefficient of X Yⁿ is (n + 1) ε, while a_{1, n} ≡ ((n + 1) / d_{n+1}) • xₙ modulo I². Hence the coefficient of bₙ in the image of y ∈ I is d_{n+1} times the n-th coordinate of the class of y in the basis (xₘ mod I²)ₘ of I ⧸ I² (TauCeti.LazardRing.coeff_single_hurewicz). In particular it is divisible by d_{n+1} on all of L, and a homogeneous y ∈ L₂ₙ is congruent to c • xₙ modulo decomposables exactly when this coefficient is c d_{n+1}: the coefficient of bₙ detects the polynomial generators of L in degree 2n.

Main definitions

• TauCeti.LazardRing.hurewicz: the Hurewicz homomorphism L →+* ℤ[b₁, b₂, …].

Main results

• TauCeti.LazardRing.map_hurewicz: it classifies the additive law transported along X + ∑ bᵢ X^(i + 1).
• TauCeti.LazardRing.map_augmentation_comp_rightUnit: it is the reduction of the right unit along the augmentation.
• TauCeti.LazardRing.isWeightedHomogeneous_hurewicz: it maps Lₙ to polynomials of degree n for bᵢ of degree 2i.
• TauCeti.LazardRing.constantCoeff_hurewicz: its constant coefficient is the augmentation.
• TauCeti.LazardRing.coeff_single_hurewicz: on the augmentation ideal, the coefficient of bₙ is d_{n+1} times the n-th coordinate in I ⧸ I².
• TauCeti.LazardRing.coeff_single_hurewicz_generator: the image of the generator xₘ has coefficient d_{n+1} at bₙ when m = n, and 0 otherwise.
• TauCeti.LazardRing.lazardGcd_dvd_coeff_single_hurewicz: the coefficient of bₙ is always divisible by d_{n+1}.
• TauCeti.LazardRing.toCotangent_eq_smul_cotangentBasis_iff_coeff_hurewicz: a homogeneous y ∈ L₂ₙ is c • xₙ modulo decomposables exactly when the coefficient of bₙ in its image is c d_{n+1}.

The injectivity of the Hurewicz homomorphism is TauCeti.LazardRing.hurewicz_injective, in TauCeti.RingTheory.FormalGroup.LazardRing.Polynomial.

References

• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1 and §3.1.
• J. F. Adams, Stable Homotopy and Generalised Homology, Part II, §§6–7.

noncomputable def TauCeti.LazardRing.hurewicz : LazardRing →+* MvPolynomial ℕ+ ℤ

The Hurewicz homomorphism L →+* ℤ[b₁, b₂, …] of the Lazard ring: the homomorphism classifying the commutative formal group law f(f⁻¹(X) + f⁻¹(Y)), the additive law transported along the strict coordinate f(X) = X + ∑_{i ≥ 1} bᵢ X^(i + 1). Through Quillen's theorem it corresponds to the Hurewicz homomorphism MU_* → H_*(MU).

@[simp]

theorem TauCeti.LazardRing.map_hurewicz : formalGroup.map hurewicz = FormalCoordinate.ofStrictCoeffs MvPolynomial.X • FormalGroup.𝔾ₐ

The Hurewicz homomorphism classifies the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1).

theorem TauCeti.LazardRing.map_augmentation_comp_rightUnit : (MvPolynomial.map augmentation).comp rightUnit = hurewicz

The Hurewicz homomorphism is the reduction of the right unit η_R : L → L[b₁, b₂, …] along the augmentation L → ℤ.

@[simp]

theorem TauCeti.LazardRing.constantCoeff_hurewicz (x : LazardRing) : MvPolynomial.constantCoeff (hurewicz x) = augmentation x

The constant coefficient of the image under the Hurewicz homomorphism is the augmentation.

The Hurewicz homomorphism is graded

theorem TauCeti.LazardRing.isWeightedHomogeneous_hurewicz {n : ℕ} {x : LazardRing} (hx : x ∈ grading n) : MvPolynomial.IsWeightedHomogeneous (fun (i : ℕ+) => 2 * ↑i) (hurewicz x) n

The Hurewicz homomorphism is graded: it maps the degree-n part Lₙ of the Lazard ring to polynomials that are homogeneous of degree n, for bᵢ of degree 2i.

The linear coefficients

theorem TauCeti.LazardRing.snd_aeval_single_eps_hurewicz (n : ℕ+) (y : LazardRing) : TrivSqZeroExt.snd ((MvPolynomial.aeval (Pi.single n DualNumber.eps)) (hurewicz y)) = (hurewicz y).coeff (Finsupp.single n 1)

The ε-component of the evaluation at bₙ = ε, bᵢ = 0 for i ≠ n, of the image of y is the coefficient of bₙ.

theorem TauCeti.LazardRing.map_aeval_single_eps_comp_hurewicz (n : ℕ+) : formalGroup.map ((MvPolynomial.aeval (Pi.single n DualNumber.eps)).comp hurewicz) = FormalCoordinate.ofStrictCoeffs (Pi.single n DualNumber.eps) • FormalGroup.𝔾ₐ

Evaluated at bₙ = ε, bᵢ = 0 for i ≠ n, the image of the universal formal group law is the additive law transported along X + ε X^(n + 1).

@[simp]

theorem TauCeti.LazardRing.coeff_single_hurewicz_generator (m n : ℕ+) : (hurewicz (generator m)).coeff (Finsupp.single n 1) = if n = m then ↑(lazardGcd (↑n + 1)) else 0

The image of a generator modulo decomposables: the image of the generator xₘ under the Hurewicz homomorphism has coefficient d_{n+1} at bₙ when m = n, and 0 otherwise. That is, xₙ ↦ d_{n+1} bₙ modulo products of the bᵢ.

theorem TauCeti.LazardRing.coeff_single_hurewicz (n : ℕ+) {y : LazardRing} (hy : y ∈ augmentationIdeal) : (hurewicz y).coeff (Finsupp.single n 1) = ↑(lazardGcd (↑n + 1)) * (cotangentBasis.repr (augmentationIdeal.toCotangent ⟨y, hy⟩)) n

The linear coefficients of the Hurewicz homomorphism compute the indecomposables: for y in the augmentation ideal I, the coefficient of bₙ in the image of y is d_{n+1} times the n-th coordinate of the class of y in the basis (xₘ mod I²)ₘ of I ⧸ I².

theorem TauCeti.LazardRing.lazardGcd_dvd_coeff_single_hurewicz (n : ℕ+) (y : LazardRing) : ↑(lazardGcd (↑n + 1)) ∣ (hurewicz y).coeff (Finsupp.single n 1)

Divisibility of the linear coefficients: the coefficient of bₙ in the image of any element of the Lazard ring under the Hurewicz homomorphism is divisible by d_{n+1}.

theorem TauCeti.LazardRing.toCotangent_eq_smul_cotangentBasis_iff_coeff_hurewicz {n : ℕ+} {y : LazardRing} (hy : y ∈ grading (2 * ↑n)) (hyI : y ∈ augmentationIdeal) (c : ℤ) : augmentationIdeal.toCotangent ⟨y, hyI⟩ = c • cotangentBasis n ↔ (hurewicz y).coeff (Finsupp.single n 1) = c * ↑(lazardGcd (↑n + 1))

The Hurewicz homomorphism detects generators: a homogeneous element y ∈ L₂ₙ is congruent to c • xₙ modulo the square of the augmentation ideal exactly when the coefficient of bₙ in its image under the Hurewicz homomorphism is c d_{n+1}. In particular y is congruent to ± xₙ modulo decomposables exactly when that coefficient is ± d_{n+1}.