Roby representability

Composition with the universal law γ_d sends a linear map Γ^d_R(M) → N to a homogeneous polynomial law of degree d. Roby's theorem says that this is a linear equivalence: every homogeneous law of degree d from M to N is represented by a unique linear map on the degree-d piece of the divided power algebra. No flatness or projectivity of M is assumed.

Uniqueness requires scalar-extended values, rather than just ground values. Evaluating at ∑ X_j ⊗ m_j and extracting a mixed coefficient recovers the value of the linear map on ∏ dp R (k j) (m j). These products span the homogeneous piece, even for modules with torsion and without inverting factorials.

The construction uses DividedPowerAlgebra.gamma and its coefficient formula. The underlying divided power algebra and polynomial laws are the Mathlib formalizations by Antoine Chambert-Loir and María Inés de Frutos-Fernández.

Main declarations

• DividedPowerAlgebra.homogeneousLawMap: the linear comparison to homogeneous laws.
• DividedPowerAlgebra.lid_rTensor_lcoeff_homogeneousLawMap: recovery by mixed coefficients.
• DividedPowerAlgebra.homogeneousLawMap_injective: uniqueness of a representing linear map.
• DividedPowerAlgebra.bilinMap_ext_gamma: bilinear maps on Γ^d_R(M) are determined by their scalar extensions on generic values of γ_d.
• DividedPowerAlgebra.homogeneousLawMap_surjective: existence of a representing linear map.
• DividedPowerAlgebra.homogeneousLawEquiv: Roby's theorem, the linear equivalence between linear maps Γ^d_R(M) → N and homogeneous laws M → N of degree d.
• DividedPowerAlgebra.homogeneousLawEquiv_symm_apply_prod_dp: the linear map representing f sends ∏ⱼ dp R kⱼ mⱼ to the coefficient of ∏ⱼ Tⱼ ^ kⱼ in f (∑ⱼ Tⱼ ⊗ mⱼ).
• DividedPowerAlgebra.homogeneousLawMap_comp and DividedPowerAlgebra.homogeneousLawMap_comp_mapHomogeneousSubmodule: naturality in both modules.
• DividedPowerAlgebra.homogeneousLawEquiv_symm_comp_mapHomogeneousSubmodule_eq_iff: the same naturality for representing linear maps.

Implementation notes

For existence, a law f determines a linear map on the polynomial ring in the variables X (n, m), sending a monomial ∏ᵢ X (nᵢ, mᵢ) to the coefficient of ∏ᵢ Tᵢ ^ nᵢ in f (∑ᵢ Tᵢ ⊗ mᵢ). Comparing coefficients along substitutions of the variables Tᵢ shows that this map respects the defining relations of Γ_R(M), even after multiplication by any monomial, so it descends to Γ_R(M). Its restriction to the degree-d piece represents f when f is homogeneous of degree d, since both laws then have the same coefficients.

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), Théorème IV.1][Roby-1963]

noncomputable def DividedPowerAlgebra.homogeneousLawMap (R : Type u) [CommSemiring R] (M : Type u_1) (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) : (↥(homogeneousSubmodule d) →ₗ[R] N) →ₗ[R] ↥(PolynomialLaw.homogeneousSubmodule R M N d)

Composition with the universal degree-d law, as a linear map into homogeneous laws. It is a linear equivalence: injectivity is homogeneousLawMap_injective, surjectivity is homogeneousLawMap_surjective, bundled as homogeneousLawEquiv.

@[simp]

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

The law associated with f is its linear polynomial law composed with γ_d.

theorem DividedPowerAlgebra.homogeneousLawMap_toFun {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (f : ↥(homogeneousSubmodule d) →ₗ[R] N) (S : Type u_4) [CommSemiring S] [Algebra R S] (x : TensorProduct R S M) : PolynomialLaw.toFun S (↑((homogeneousLawMap R M N d) f)) x = (LinearMap.baseChange S f) (PolynomialLaw.toFun S (gamma R M d) x)

At any scalar algebra, the comparison is the base change of f applied to γ_d.

@[simp]

theorem DividedPowerAlgebra.ground_toPolynomialLaw_comp_gamma_apply {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (f : ↥(homogeneousSubmodule d) →ₗ[R] N) (m : M) : (f.toPolynomialLaw.comp (gamma R M d)).ground m = f ⟨dp R d m, ⋯⟩

The ground value of the associated law is f evaluated on the divided-power generator.

theorem DividedPowerAlgebra.lid_rTensor_lcoeff_homogeneousLawMap {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (f : ↥(homogeneousSubmodule d) →ₗ[R] N) {ι : Type u_4} [Fintype ι] (m : ι → M) (k : ι →₀ ℕ) (hk : ∑ j : ι, k j = d) : (TensorProduct.lid R N) ((LinearMap.rTensor N (MvPolynomial.lcoeff R k)) (PolynomialLaw.toFun (MvPolynomial ι R) (↑((homogeneousLawMap R M N d) f)) (∑ j : ι, MvPolynomial.X j ⊗ₜ[R] m j))) = f ⟨∏ j : ι, dp R (k j) (m j), ⋯⟩

Mixed coefficients of the associated law recover f on products of divided powers. The hypothesis fixes the total degree of the monomial, with no factorial factors.

theorem DividedPowerAlgebra.homogeneousLawMap_injective {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) : Function.Injective ⇑(homogeneousLawMap R M N d)

Composition with γ_d determines a linear map on the entire homogeneous piece. Ground values alone need not determine it; the proof uses mixed coefficients over polynomial scalar algebras.

theorem DividedPowerAlgebra.bilinMap_ext_gamma {R : Type u} [CommSemiring R] {M : Type u_1} {P : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (d : ℕ) {β β' : LinearMap.BilinMap R (↥(homogeneousSubmodule d)) P} (h : ∀ (p q : ℕ) (m : Fin p → M) (n : Fin q → M), ((LinearMap.BilinMap.baseChange (MvPolynomial (Fin p ⊕ Fin q) R) β) (PolynomialLaw.toFun (MvPolynomial (Fin p ⊕ Fin q) R) (gamma R M d) (∑ i : Fin p, MvPolynomial.X (Sum.inl i) ⊗ₜ[R] m i))) (PolynomialLaw.toFun (MvPolynomial (Fin p ⊕ Fin q) R) (gamma R M d) (∑ j : Fin q, MvPolynomial.X (Sum.inr j) ⊗ₜ[R] n j)) = ((LinearMap.BilinMap.baseChange (MvPolynomial (Fin p ⊕ Fin q) R) β') (PolynomialLaw.toFun (MvPolynomial (Fin p ⊕ Fin q) R) (gamma R M d) (∑ i : Fin p, MvPolynomial.X (Sum.inl i) ⊗ₜ[R] m i))) (PolynomialLaw.toFun (MvPolynomial (Fin p ⊕ Fin q) R) (gamma R M d) (∑ j : Fin q, MvPolynomial.X (Sum.inr j) ⊗ₜ[R] n j))) : β = β'

Bilinear maps on Γ^d_R(M) are determined by their scalar extensions evaluated at γ_d(u) and γ_d(v), for generic combinations u and v in two disjoint groups of variables.

theorem DividedPowerAlgebra.homogeneousLawMap_comp {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (d : ℕ) (f : ↥(homogeneousSubmodule d) →ₗ[R] N) (g : N →ₗ[R] P) : ↑((homogeneousLawMap R M P d) (g ∘ₗ f)) = g.toPolynomialLaw.comp ↑((homogeneousLawMap R M N d) f)

Postcomposition of the representing linear map agrees with postcomposition of its law.

theorem DividedPowerAlgebra.homogeneousLawMap_comp_mapHomogeneousSubmodule {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (d : ℕ) (f : M →ₗ[R] N) (g : ↥(homogeneousSubmodule d) →ₗ[R] P) : ↑((homogeneousLawMap R M P d) (g ∘ₗ mapHomogeneousSubmodule f d)) = (↑((homogeneousLawMap R N P d) g)).comp f.toPolynomialLaw

Precomposition on homogeneous pieces agrees with precomposition of polynomial laws.

theorem DividedPowerAlgebra.homogeneousLawMap_surjective {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) : Function.Surjective ⇑(homogeneousLawMap R M N d)

Every homogeneous polynomial law of degree d is represented by a linear map on Γ^d_R(M): the comparison homogeneousLawMap is surjective.

noncomputable def DividedPowerAlgebra.homogeneousLawEquiv (R : Type u) [CommSemiring R] (M : Type u_1) (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) : (↥(homogeneousSubmodule d) →ₗ[R] N) ≃ₗ[R] ↥(PolynomialLaw.homogeneousSubmodule R M N d)

Roby representability: composition with the universal law γ_d is a linear equivalence between linear maps Γ^d_R(M) → N and homogeneous polynomial laws M → N of degree d.

@[simp]

theorem DividedPowerAlgebra.homogeneousLawEquiv_apply {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (g : ↥(homogeneousSubmodule d) →ₗ[R] N) : (homogeneousLawEquiv R M N d) g = (homogeneousLawMap R M N d) g

theorem DividedPowerAlgebra.homogeneousLawEquiv_symm_apply_prod_dp {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (f : ↥(PolynomialLaw.homogeneousSubmodule R M N d)) {ι : Type u_4} [Fintype ι] (m : ι → M) (k : ι →₀ ℕ) (hk : ∑ j : ι, k j = d) : ((homogeneousLawEquiv R M N d).symm f) ⟨∏ j : ι, dp R (k j) (m j), ⋯⟩ = ((PolynomialLaw.coeff R N m) ↑f) k

The linear map representing a homogeneous law f of degree d sends ∏ⱼ dp R kⱼ mⱼ, with ∑ⱼ kⱼ = d, to the coefficient of ∏ⱼ Tⱼ ^ kⱼ in f (∑ⱼ Tⱼ ⊗ mⱼ).

@[simp]

theorem DividedPowerAlgebra.homogeneousLawEquiv_symm_apply_dp {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d : ℕ) (f : ↥(PolynomialLaw.homogeneousSubmodule R M N d)) (m : M) : ((homogeneousLawEquiv R M N d).symm f) ⟨dp R d m, ⋯⟩ = (↑f).ground m

The linear map representing a homogeneous law f of degree d sends dp R d m to the ground value f m.

theorem DividedPowerAlgebra.homogeneousLawEquiv_symm_comp_mapHomogeneousSubmodule_eq_iff {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (d : ℕ) {Q : Type u_4} [AddCommMonoid Q] [Module R Q] (f : M →ₗ[R] N) (g : P →ₗ[R] Q) (F : ↥(PolynomialLaw.homogeneousSubmodule R N Q d)) (G : ↥(PolynomialLaw.homogeneousSubmodule R M P d)) : (homogeneousLawEquiv R N Q d).symm F ∘ₗ mapHomogeneousSubmodule f d = g ∘ₗ (homogeneousLawEquiv R M P d).symm G ↔ (↑F).comp f.toPolynomialLaw = g.toPolynomialLaw.comp ↑G

Representability is natural: the linear maps representing homogeneous laws F on N and G on M intertwine Γ^d(f) and g exactly when the laws intertwine f and g.