Coefficients of polynomial laws

For a polynomial law f : M →ₚₗ[R] N and a finite family m : ι → M, the value of f at the generic combination ∑ⱼ Xⱼ ⊗ mⱼ over the polynomial ring R[Xⱼ] is a finite sum ∑ₖ Xᵏ ⊗ cₖ. The coefficients cₖ = coeff m f k determine f: after scalar extension to any commutative R-algebra S, f (∑ⱼ sⱼ ⊗ mⱼ) = ∑ₖ (∏ⱼ sⱼ ^ kⱼ) ⊗ coeff m f k.

These coefficients are the values of the linear maps out of divided powers which represent homogeneous polynomial laws, so this file supplies the comparison tools used to construct them: the change-of-variables formula for coefficients, the fact that a law is determined by its coefficients, and the vanishing of the coefficients of a homogeneous law of degree d outside total degree d.

The underlying PolynomialLaws are the Mathlib formalization by Antoine Chambert-Loir and María Inés de Frutos-Fernández. The coefficient map PolynomialLaw.coeff, the evaluation formula PolynomialLaw.toFun_sum_tmul_eq_coeff_sum, the extensionality lemma and the vanishing of coefficients of homogeneous laws follow the coefficient API of their polynomial-law formalization in the DividedPowers project.

Main declarations

• PolynomialLaw.coeff m: the coefficients of a law at the generic combination of m, as an R-linear map to finitely supported functions on monomials.
• PolynomialLaw.coeff_apply: the coefficient of Xᵏ, extracted by MvPolynomial.lcoeff.
• PolynomialLaw.toFun_sum_tmul_eq_coeff_sum: the value of a law on any finite sum of pure tensors, in terms of its coefficients.
• PolynomialLaw.coeff_eq_sum_of_sum_tmul_eq: change of variables for coefficients, and PolynomialLaw.coeff_eq_smul_of_sum_tmul_eq, its form when a single monomial survives.
• PolynomialLaw.coeff_comp_equiv, PolynomialLaw.coeff_optionElim_zero, PolynomialLaw.coeff_optionElim_smul, PolynomialLaw.coeff_optionElim_optionElim_self and PolynomialLaw.coeff_optionElim_add: coefficients are invariant under reindexing, ignore vectors with exponent zero, scale by r ^ n with a vector scaled by r, merge two equal vectors with a binomial coefficient, and split a sum of vectors along the antidiagonal.
• PolynomialLaw.ext_coeff: a law is determined by its coefficients on families indexed by Fin n.
• PolynomialLaw.IsHomogeneousOfDegree.coeff_eq_zero: a law homogeneous of degree d has no coefficients outside total degree d.

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), Chapitre I][Roby-1963]

noncomputable def PolynomialLaw.coeff (R : Type u) [CommSemiring R] {M : Type u_1} (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (m : ι → M) : (M →ₚₗ[R] N) →ₗ[R] (ι →₀ ℕ) →₀ N

The coefficients of polynomial laws M →ₚₗ[R] N at the generic combination ∑ⱼ Xⱼ ⊗ mⱼ: coeff m f k is the coefficient of the monomial Xᵏ in f (∑ⱼ Xⱼ ⊗ mⱼ), computed over the polynomial ring R[Xⱼ].

theorem PolynomialLaw.coeff_apply {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N m) f) k = (TensorProduct.lid R N) ((LinearMap.rTensor N (MvPolynomial.lcoeff R k)) (toFun (MvPolynomial ι R) f (∑ j : ι, MvPolynomial.X j ⊗ₜ[R] m j)))

The coefficient of Xᵏ in f (∑ⱼ Xⱼ ⊗ mⱼ), extracted by MvPolynomial.lcoeff.

theorem PolynomialLaw.toFun_sum_X_tmul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (m : ι → M) (f : M →ₚₗ[R] N) : toFun (MvPolynomial ι R) f (∑ j : ι, MvPolynomial.X j ⊗ₜ[R] m j) = ((coeff R N m) f).sum fun (k : ι →₀ ℕ) (n : N) => (MvPolynomial.monomial k) 1 ⊗ₜ[R] n

The value of f at the generic combination ∑ⱼ Xⱼ ⊗ mⱼ is ∑ₖ Xᵏ ⊗ coeff m f k.

theorem PolynomialLaw.toFun_sum_tmul_eq_coeff_sum {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (m : ι → M) (f : M →ₚₗ[R] N) {S : Type u_4} [CommSemiring S] [Algebra R S] (s : ι → S) : toFun S f (∑ j : ι, s j ⊗ₜ[R] m j) = ((coeff R N m) f).sum fun (k : ι →₀ ℕ) (n : N) => (∏ j : ι, s j ^ k j) ⊗ₜ[R] n

The value of a polynomial law on a finite sum of pure tensors, in terms of its coefficients: f (∑ⱼ sⱼ ⊗ mⱼ) = ∑ₖ (∏ⱼ sⱼ ^ kⱼ) ⊗ coeff m f k, for a commutative R-algebra S in any universe.

theorem PolynomialLaw.coeff_eq_sum_of_sum_tmul_eq {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] {κ : Type u_4} [Fintype κ] (f : M →ₚₗ[R] N) (m : ι → M) (s : ι → MvPolynomial κ R) (m' : κ → M) (h : ∑ j : ι, s j ⊗ₜ[R] m j = ∑ i : κ, MvPolynomial.X i ⊗ₜ[R] m' i) (k : κ →₀ ℕ) : ((coeff R N m') f) k = ((coeff R N m) f).sum fun (l : ι →₀ ℕ) (n : N) => (∏ j : ι, s j ^ l j).coeff k • n

Change of variables for coefficients: if the generic combination of m' is obtained from ∑ⱼ sⱼ ⊗ mⱼ for polynomials sⱼ, then each coefficient of f at m' is a combination of the coefficients of f at m.

theorem PolynomialLaw.coeff_eq_smul_of_sum_tmul_eq {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] {κ : Type u_4} [Fintype κ] [DecidableEq ι] (f : M →ₚₗ[R] N) (m : ι → M) (s : ι → MvPolynomial κ R) (m' : κ → M) (h : ∑ j : ι, s j ⊗ₜ[R] m j = ∑ i : κ, MvPolynomial.X i ⊗ₜ[R] m' i) (k : κ →₀ ℕ) (l₀ : ι →₀ ℕ) (c : R) (hc : ∀ (l : ι →₀ ℕ), (∏ j : ι, s j ^ l j).coeff k = if l = l₀ then c else 0) : ((coeff R N m') f) k = c • ((coeff R N m) f) l₀

Change of variables with a single surviving monomial: if the coefficient of Xᵏ in ∏ⱼ sⱼ ^ lⱼ is c for l = l₀ and zero for every other l, then coeff m' f k = c • coeff m f l₀.

theorem PolynomialLaw.coeff_comp_equiv {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] {κ : Type u_4} [Fintype κ] (e : κ ≃ ι) (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N (m ∘ ⇑e)) f) (Finsupp.equivMapDomain e.symm k) = ((coeff R N m) f) k

Coefficients are invariant under reindexing the family along an equivalence.

theorem PolynomialLaw.coeff_optionElim_zero {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (a : M) (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N (Option.elim' a m)) f) (Finsupp.optionElim 0 k) = ((coeff R N m) f) k

A vector with exponent zero does not contribute to a coefficient.

theorem PolynomialLaw.coeff_optionElim_smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (n : ℕ) (r : R) (a : M) (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N (Option.elim' (r • a) m)) f) (Finsupp.optionElim n k) = r ^ n • ((coeff R N (Option.elim' a m)) f) (Finsupp.optionElim n k)

Scaling a vector with exponent n by r scales the coefficient by r ^ n.

theorem PolynomialLaw.coeff_optionElim_optionElim_self {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (x y : ℕ) (a : M) (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N (Option.elim' a (Option.elim' a m))) f) (Finsupp.optionElim x (Finsupp.optionElim y k)) = (x + y).choose x • ((coeff R N (Option.elim' a m)) f) (Finsupp.optionElim (x + y) k)

Two copies of the same vector, with exponents x and y, merge into one with exponent x + y, at the cost of the binomial coefficient (x + y).choose x.

theorem PolynomialLaw.coeff_optionElim_add {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] (n : ℕ) (a b : M) (m : ι → M) (f : M →ₚₗ[R] N) (k : ι →₀ ℕ) : ((coeff R N (Option.elim' (a + b) m)) f) (Finsupp.optionElim n k) = ∑ q ∈ Finset.antidiagonal n, ((coeff R N (Option.elim' a (Option.elim' b m))) f) (Finsupp.optionElim q.1 (Finsupp.optionElim q.2 k))

A vector a + b with exponent n splits into the vectors a and b, summed over the exponent pairs in the antidiagonal of n, as in the divided-power binomial formula.

theorem PolynomialLaw.ext_coeff {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M →ₚₗ[R] N} (h : ∀ (n : ℕ) (m : Fin n → M), (coeff R N m) f = (coeff R N m) g) : f = g

A polynomial law is determined by its coefficients on families indexed by Fin n.

theorem PolynomialLaw.IsHomogeneousOfDegree.coeff_eq_zero {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Fintype ι] {d : ℕ} {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree d f) (m : ι → M) {k : ι →₀ ℕ} (hk : ∑ j : ι, k j ≠ d) : ((coeff R N m) f) k = 0

A law homogeneous of degree d has no coefficients outside total degree d.