The Kronecker substitution

For a weight e : σ → ℕ, the Kronecker substitution Xₛ ↦ T ^ eₛ turns a multivariate polynomial into a polynomial in one variable T, sending the monomial c X^μ to c T ^ (weight e μ) (MvPolynomial.aeval_X_pow_left_monomial). It is injective on the polynomials supported in any set of exponent vectors on which weight e is injective, and every finite set of exponent vectors admits such a weight. Consequently a finite family of multivariate polynomials can be carried to a family of univariate polynomials while preserving linear independence. This reduces statements about several variables, such as the generalized Wronskian criterion, to the one-variable case.

Translating T to T + a turns the substitution into Xₛ ↦ (T + a) ^ eₛ - a ^ eₛ applied to the Taylor expansion of f at (a ^ eₛ)ₛ. This gives a chain rule: Hasse derivatives of the image of f, evaluated at a, are linear combinations of the Hasse derivatives of f evaluated at (a ^ eₛ)ₛ.

Main results

• Finsupp.exists_injOn_weight: every finite set of exponent vectors is separated by weight e for some e : σ → ℕ.
• MvPolynomial.coeff_aeval_X_pow_weight: if weight e is injective on a set containing the support of f and μ, the coefficient of T ^ (weight e μ) is that of X^μ in f.
• MvPolynomial.injOn_aeval_X_pow, MvPolynomial.linearIndependent_aeval_X_pow: the substitution is injective on such polynomials and preserves linear independence of families supported there.
• MvPolynomial.taylor_aeval_X_pow: the substitution intertwines the Taylor expansions at a and at (a ^ eₛ)ₛ.
• MvPolynomial.eval_hasseDeriv_aeval_X_pow: the chain rule for the substitution; the k-th Hasse derivative of the image only involves Hasse derivatives ∂^ν f with |ν| ≤ k (MvPolynomial.coeff_aeval_X_add_C_pow_sub_C_eq_zero).

Implementation notes

The variables may form an arbitrary type. A separating weight is a Lazard evaluator (TauCeti.exists_isLazardEvaluator, TauCeti.IsLazardEvaluator.weight_injOn) for a linear order on the variables chosen locally from a well-ordering; the statement does not depend on that order.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (version of 17 January 2022), §3.3, Exercise 3.5, which uses the weights eⱼ = Bʲ for B larger than all partial degrees.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), proof of Proposition 6.3.10.
• The injectivity of the substitution on separated supports and its use for linear independence are adapted from Ralf Stephan's DiophantineApproximation/GeneralizedWronskian.lean in rwst/Subspace-Theorems, commit 5cff93ceb4b69b2048473301411763febe96bb3f (Apache 2.0).

theorem Finsupp.exists_injOn_weight {σ : Type u_1} (T : Finset (σ →₀ ℕ)) : ∃ (e : σ → ℕ), Set.InjOn ⇑(weight e) ↑T

Every finite set of exponent vectors is separated by a single weight: some e : σ → ℕ makes weight e injective on it. No order on the variables is needed.

theorem MvPolynomial.coeff_aeval_X_pow_weight {R : Type u_1} {σ : Type u_2} [CommSemiring R] {e : σ → ℕ} {T : Set (σ →₀ ℕ)} (he : Set.InjOn (⇑(Finsupp.weight e)) T) {f : MvPolynomial σ R} (hf : ↑f.support ⊆ T) {μ : σ →₀ ℕ} (hμ : μ ∈ T) : ((aeval fun (s : σ) => Polynomial.X ^ e s) f).coeff ((Finsupp.weight e) μ) = f.coeff μ

If weight e is injective on a set T containing the support of f and the exponent μ, then after the Kronecker substitution Xₛ ↦ T ^ eₛ the coefficient of T ^ (weight e μ) is the coefficient of X^μ in f.

theorem MvPolynomial.injOn_aeval_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] {e : σ → ℕ} {T : Set (σ →₀ ℕ)} (he : Set.InjOn (⇑(Finsupp.weight e)) T) : Set.InjOn ⇑(aeval fun (s : σ) => Polynomial.X ^ e s) ↑(restrictSupport R T)

The Kronecker substitution Xₛ ↦ T ^ eₛ is injective on the polynomials supported in a set of exponent vectors on which weight e is injective.

theorem MvPolynomial.linearIndependent_aeval_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] {ι : Type u_3} {e : σ → ℕ} {T : Set (σ →₀ ℕ)} (he : Set.InjOn (⇑(Finsupp.weight e)) T) {φ : ι → MvPolynomial σ R} (hφT : ∀ (i : ι), ↑(φ i).support ⊆ T) (hφ : LinearIndependent R φ) : LinearIndependent R fun (i : ι) => (aeval fun (s : σ) => Polynomial.X ^ e s) (φ i)

The Kronecker substitution Xₛ ↦ T ^ eₛ preserves linear independence of a family of polynomials supported in a set of exponent vectors on which weight e is injective.

theorem MvPolynomial.taylor_aeval_X_pow {R : Type u_1} {σ : Type u_2} [CommRing R] (e : σ → ℕ) (a : R) (f : MvPolynomial σ R) : (Polynomial.taylor a) ((aeval fun (s : σ) => Polynomial.X ^ e s) f) = (aeval fun (s : σ) => (Polynomial.X + Polynomial.C a) ^ e s - Polynomial.C (a ^ e s)) ((taylor fun (s : σ) => a ^ e s) f)

Translating T to T + a after the Kronecker substitution Xₛ ↦ T ^ eₛ is the same as translating X to X + (a ^ eₛ)ₛ and then substituting Xₛ ↦ (T + a) ^ eₛ - a ^ eₛ.

theorem MvPolynomial.coeff_aeval_X_add_C_pow_sub_C_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] (e : σ → ℕ) (a : R) (ν : σ →₀ ℕ) {k : ℕ} (hk : k < Finsupp.degree ν) : ((aeval fun (s : σ) => (Polynomial.X + Polynomial.C a) ^ e s - Polynomial.C (a ^ e s)) ((monomial ν) 1)).coeff k = 0

The translated Kronecker substitution Xₛ ↦ (T + a) ^ eₛ - a ^ eₛ sends X^ν to a multiple of T ^ |ν|, so the coefficients of T ^ k with k < |ν| vanish.

theorem MvPolynomial.eval_hasseDeriv_aeval_X_pow {R : Type u_1} {σ : Type u_2} [CommRing R] (e : σ → ℕ) (a : R) (f : MvPolynomial σ R) (k : ℕ) {T : Finset (σ →₀ ℕ)} (hT : ((taylor fun (s : σ) => a ^ e s) f).support ⊆ T) : Polynomial.eval a ((Polynomial.hasseDeriv k) ((aeval fun (s : σ) => Polynomial.X ^ e s) f)) = ∑ ν ∈ T, ((aeval fun (s : σ) => (Polynomial.X + Polynomial.C a) ^ e s - Polynomial.C (a ^ e s)) ((monomial ν) 1)).coeff k * (eval fun (s : σ) => a ^ e s) ((hasseDeriv ν) f)

The chain rule for the Kronecker substitution. The k-th Hasse derivative of the image of f under Xₛ ↦ T ^ eₛ, evaluated at a, is a linear combination of the Hasse derivatives ∂^ν f evaluated at (a ^ eₛ)ₛ, with coefficients independent of f.