The universal homogeneous polynomial law

For a module M over a commutative semiring R and d : ℕ, this file constructs the universal homogeneous polynomial law γ_d : M → Γ^d_R(M) of degree d, with values in the degree-d homogeneous piece of the divided power algebra. After scalar extension to a commutative R-algebra S it is given by γ_d(∑ⱼ sⱼ ⊗ mⱼ) = ∑_{∑ⱼ nⱼ = d} (∏ⱼ sⱼ ^ nⱼ) ⊗ ∏ⱼ dp nⱼ mⱼ, so that its ground value is γ_d(m) = dp R d m, and over a polynomial ring the coefficient of ∏ⱼ Tⱼ ^ nⱼ in γ_d(∑ⱼ Tⱼ ⊗ mⱼ) is ∏ⱼ dp nⱼ mⱼ when ∑ⱼ nⱼ = d, and zero otherwise. No factorial is inverted: over ℤ the coefficient of U V in γ_2(U ⊗ x + V ⊗ y) is dp 1 x * dp 1 y, with no factor 2.

Roby's representability theorem identifies the degree-d homogeneous laws M → N with the linear maps Γ^d_R(M) → N, by composition with γ_d.

Main declarations

• DividedPowerAlgebra.gamma R M d: the universal homogeneous polynomial law of degree d.
• DividedPowerAlgebra.isHomogeneousOfDegree_gamma: it is homogeneous of degree d.
• DividedPowerAlgebra.gamma_toFun_tmul: γ_d(s ⊗ m) = s ^ d ⊗ dp R d m.
• DividedPowerAlgebra.gamma_toFun_one: for an algebra A, γ_d(1) = 1 ⊗ dp R d 1.
• DividedPowerAlgebra.gamma_toFun_sum_tmul: the formula for γ_d on a finite sum of pure tensors, after scalar extension to an algebra in any universe.
• DividedPowerAlgebra.ground_gamma_apply: the ground value of γ_d at m is dp R d m.
• DividedPowerAlgebra.gamma_comp_toPolynomialLaw: naturality in the source module.
• DividedPowerAlgebra.coe_lid_rTensor_lcoeff_gamma_toFun_sum_X_tmul: the coefficient of the monomial ∏ⱼ Tⱼ ^ kⱼ in γ_d(∑ⱼ Tⱼ ⊗ mⱼ) is ∏ⱼ dp kⱼ mⱼ when ∑ⱼ kⱼ = d, and 0 otherwise.

Implementation notes

The values of all the laws γ_d are packaged into the divided-power exponential DividedPowerAlgebra.exp, exp(x) = ∑_d γ_d(x) X ^ d, a power series with coefficients in S ⊗[R] Γ_R(M), which is defined on pure tensors by exp(s ⊗ m) = ∑ₙ (s ^ n ⊗ dp R n m) X ^ n. The law γ_d is the X ^ d-coefficient of exp, projected to the degree-d piece through the direct-sum grading of Γ_R(M).

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), Proposition IV.1 and Théorème IV.1][Roby-1963]
• The ambient DividedPowerAlgebra and the PolynomialLaws are the Mathlib formalizations by Antoine Chambert-Loir and María Inés de Frutos-Fernández.

noncomputable def DividedPowerAlgebra.gamma (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] (d : ℕ) : M →ₚₗ[R] ↥(homogeneousSubmodule d)

The universal homogeneous polynomial law γ_d : M → Γ^d_R(M) of degree d. After scalar extension to a commutative R-algebra S it sends ∑ⱼ sⱼ ⊗ mⱼ to ∑_{∑ⱼ nⱼ = d} (∏ⱼ sⱼ ^ nⱼ) ⊗ ∏ⱼ dp R nⱼ mⱼ (see gamma_toFun_sum_tmul), and its ground value is m ↦ dp R d m (see ground_gamma_apply).

theorem DividedPowerAlgebra.isHomogeneousOfDegree_gamma {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (d : ℕ) : PolynomialLaw.IsHomogeneousOfDegree d (gamma R M d)

The universal law γ_d is homogeneous of degree d.

theorem DividedPowerAlgebra.gamma_toFun_sum_tmul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (d : ℕ) {S : Type u_2} [CommSemiring S] [Algebra R S] {ι : Type u_3} [DecidableEq ι] (t : Finset ι) (s : ι → S) (m : ι → M) : PolynomialLaw.toFun S (gamma R M d) (∑ j ∈ t, s j ⊗ₜ[R] m j) = ∑ l ∈ t.finsuppAntidiag d, (∏ j ∈ t, s j ^ l j) ⊗ₜ[R] ((DirectSum.decompose homogeneousSubmodule) (∏ j ∈ t, dp R (l j) (m j))) d

The value of γ_d on a finite sum of pure tensors: γ_d(∑ⱼ sⱼ ⊗ mⱼ) = ∑_{∑ⱼ nⱼ = d} (∏ⱼ sⱼ ^ nⱼ) ⊗ ∏ⱼ dp R nⱼ mⱼ. Each product ∏ⱼ dp R nⱼ mⱼ lies in the degree-d piece, where it is its own degree-d component.

@[simp]

theorem DividedPowerAlgebra.gamma_toFun_tmul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (d : ℕ) {S : Type u_2} [CommSemiring S] [Algebra R S] (s : S) (m : M) : PolynomialLaw.toFun S (gamma R M d) (s ⊗ₜ[R] m) = (s ^ d) ⊗ₜ[R] ⟨dp R d m, ⋯⟩

The value of γ_d on a pure tensor: γ_d(s ⊗ m) = s ^ d ⊗ dp R d m.

@[simp]

theorem DividedPowerAlgebra.gamma_toFun_one {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (d : ℕ) (S : Type u_3) [CommSemiring S] [Algebra R S] : PolynomialLaw.toFun S (gamma R A d) 1 = 1 ⊗ₜ[R] ⟨dp R d 1, ⋯⟩

For an R-algebra A, the value of γ_d at the unit of S ⊗[R] A is 1 ⊗ dp R d 1.

@[simp]

theorem DividedPowerAlgebra.ground_gamma_apply {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (d : ℕ) (m : M) : (gamma R M d).ground m = ⟨dp R d m, ⋯⟩

The ground value of γ_d at m is dp R d m.

theorem DividedPowerAlgebra.coe_lid_rTensor_lcoeff_gamma_toFun_sum_X_tmul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (d : ℕ) {ι : Type u_2} [Fintype ι] (m : ι → M) (k : ι →₀ ℕ) : ↑((TensorProduct.lid R ↥(homogeneousSubmodule d)) ((LinearMap.rTensor (↥(homogeneousSubmodule d)) (MvPolynomial.lcoeff R k)) (PolynomialLaw.toFun (MvPolynomial ι R) (gamma R M d) (∑ j : ι, MvPolynomial.X j ⊗ₜ[R] m j)))) = if ∑ j : ι, k j = d then ∏ j : ι, dp R (k j) (m j) else 0

The coefficient of the monomial ∏ⱼ Tⱼ ^ kⱼ in γ_d(∑ⱼ Tⱼ ⊗ mⱼ), computed over the polynomial ring R[Tⱼ], is ∏ⱼ dp R kⱼ mⱼ when ∑ⱼ kⱼ = d, and 0 otherwise.

theorem DividedPowerAlgebra.gamma_comp_toPolynomialLaw {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (d : ℕ) : (gamma R N d).comp f.toPolynomialLaw = (mapHomogeneousSubmodule f d).toPolynomialLaw.comp (gamma R M d)

The universal homogeneous law is natural in its source module.