Linear changes of variables in multivariate polynomials

For a square matrix M indexed by the variables, MvPolynomial.linearSubst M is the R-algebra endomorphism of R[Xᵢ : i ∈ σ] substituting Xᵢ ↦ ∑ⱼ Mᵢⱼ Xⱼ. Evaluated at a point x, the polynomial linearSubst M p is p evaluated at M *ᵥ x: the substitution is the pullback of polynomial functions along M. It is therefore a right action of the matrix monoid, linearSubst (M * N) = (linearSubst N).comp (linearSubst M).

The substitution preserves homogeneity, and on forms of degree n a scalar matrix c • 1 acts by cⁿ. Restricted to the forms of a fixed degree n it is the representation MvPolynomial.linearSubstRep of the opposite matrix monoid on homogeneousSubmodule σ R n. In two variables this is the action P ↦ P(aX + bY, cX + dY) of 2 × 2 matrices on binary forms of degree n, through which the modular group acts on period polynomials.

Main definitions

• MvPolynomial.linearSubst: the substitution Xᵢ ↦ ∑ⱼ Mᵢⱼ Xⱼ.
• MvPolynomial.linearSubstRep: its restriction to forms of degree n, as a representation of (Matrix σ σ R)ᵐᵒᵖ.

Main results

• MvPolynomial.aeval_linearSubst: linearSubst M p evaluated at x is p evaluated at M *ᵥ x.
• MvPolynomial.linearSubst_mul: the substitution is a right action.
• MvPolynomial.map_linearSubst: changing coefficients commutes with substitution.
• MvPolynomial.linearSubst_diagonal_monomial: a diagonal matrix scales each monomial by the product of its diagonal entries raised to the corresponding exponents.
• MvPolynomial.coeff_linearSubst_upperTriangular_monomial: under an upper-triangular substitution in two variables, the coefficient of X₀ᵏ X₁ˡ in its own image is aᵏ dˡ.
• MvPolynomial.IsHomogeneous.linearSubst: the substitution preserves homogeneity.
• MvPolynomial.IsHomogeneous.linearSubst_smul: rescaling the matrix by c rescales a form of degree n by cⁿ.
• MvPolynomial.eq_zero_of_add_self_eq_zero: a polynomial is zero if adding it to itself is zero and multiplication by 2 is injective on coefficients.

theorem MvPolynomial.eq_zero_of_add_self_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (h2 : Function.Injective fun (r : R) => 2 * r) {p : MvPolynomial σ R} (h : p + p = 0) : p = 0

A polynomial is zero if adding it to itself is zero and multiplication by 2 is injective on coefficients.

noncomputable def MvPolynomial.linearSubst {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M : Matrix σ σ R) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R

The linear change of variables Xᵢ ↦ ∑ⱼ Mᵢⱼ Xⱼ given by a square matrix M.

Equations

• MvPolynomial.linearSubst M = MvPolynomial.aeval fun (i : σ) => ∑ j : σ, MvPolynomial.C (M i j) * MvPolynomial.X j

theorem MvPolynomial.linearSubst_eq_aeval {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M : Matrix σ σ R) : linearSubst M = aeval fun (i : σ) => ∑ j : σ, C (M i j) * X j

@[simp]

theorem MvPolynomial.linearSubst_X {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M : Matrix σ σ R) (i : σ) : (linearSubst M) (X i) = ∑ j : σ, C (M i j) * X j

theorem MvPolynomial.map_linearSubst {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (M : Matrix σ σ R) (p : MvPolynomial σ R) : (map f) ((linearSubst M) p) = (linearSubst (M.map ⇑f)) ((map f) p)

Changing the coefficients commutes with substitution, after mapping the matrix entries.

@[simp]

theorem MvPolynomial.linearSubst_diagonal_monomial {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] [DecidableEq σ] (v : σ → R) (s : σ →₀ ℕ) : (linearSubst (Matrix.diagonal v)) ((monomial s) 1) = (s.prod fun (i : σ) (k : ℕ) => v i ^ k) • (monomial s) 1

A diagonal change of variables scales a monomial by the product of its eigenvalues.

theorem MvPolynomial.coeff_linearSubst_upperTriangular_monomial {R : Type u_2} [CommSemiring R] (a b d : R) (s : Fin 2 →₀ ℕ) : ((linearSubst !![a, b; 0, d]) ((monomial s) 1)).coeff s = a ^ s 0 * d ^ s 1

An upper-triangular change of variables in two variables is triangular on monomials: the coefficient of X₀ᵏ X₁ˡ in the image of X₀ᵏ X₁ˡ is aᵏ dˡ, independently of b.

theorem MvPolynomial.aeval_linearSubst {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] (M : Matrix σ σ R) (x : σ → S) (p : MvPolynomial σ R) : (aeval x) ((linearSubst M) p) = (aeval ((M.map ⇑(algebraMap R S)).mulVec x)) p

Evaluating linearSubst M p at x is evaluating p at M *ᵥ x.

theorem MvPolynomial.eval_linearSubst {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M : Matrix σ σ R) (x : σ → R) (p : MvPolynomial σ R) : (eval x) ((linearSubst M) p) = (eval (M.mulVec x)) p

Evaluating linearSubst M p at x is evaluating p at M *ᵥ x.

@[simp]

theorem MvPolynomial.linearSubst_one {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] [DecidableEq σ] : linearSubst 1 = AlgHom.id R (MvPolynomial σ R)

theorem MvPolynomial.linearSubst_mul {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M N : Matrix σ σ R) : linearSubst (M * N) = (linearSubst N).comp (linearSubst M)

The substitution is a right action of the matrix monoid: substituting along M * N is substituting along M and then along N.

theorem MvPolynomial.linearSubst_mul_apply {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (M N : Matrix σ σ R) (p : MvPolynomial σ R) : (linearSubst (M * N)) p = (linearSubst N) ((linearSubst M) p)

theorem MvPolynomial.IsHomogeneous.linearSubst {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (M : Matrix σ σ R) : ((MvPolynomial.linearSubst M) p).IsHomogeneous n

A linear change of variables preserves homogeneity.

theorem MvPolynomial.IsHomogeneous.aeval_C_mul_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (c : R) : (MvPolynomial.aeval fun (i : σ) => C c * X i) p = c ^ n • p

Substituting Xᵢ ↦ c Xᵢ in a form of degree n multiplies it by cⁿ.

theorem MvPolynomial.IsHomogeneous.linearSubst_smul {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (c : R) (M : Matrix σ σ R) : (MvPolynomial.linearSubst (c • M)) p = c ^ n • (MvPolynomial.linearSubst M) p

Rescaling the matrix by c rescales a form of degree n by cⁿ.

theorem MvPolynomial.IsHomogeneous.linearSubst_neg {σ : Type u_1} [Fintype σ] {R : Type u_3} [CommRing R] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (M : Matrix σ σ R) : (MvPolynomial.linearSubst (-M)) p = (-1) ^ n • (MvPolynomial.linearSubst M) p

On forms of degree n, negating the matrix multiplies by (-1)ⁿ.

noncomputable def MvPolynomial.linearSubstRep (σ : Type u_1) (R : Type u_2) [Fintype σ] [CommSemiring R] [DecidableEq σ] (n : ℕ) : Representation R (Matrix σ σ R)ᵐᵒᵖ ↥(homogeneousSubmodule σ R n)

The linear changes of variables restricted to the forms of degree n, as a representation of the opposite matrix monoid: op M acts by p ↦ linearSubst M p.

Equations

• MvPolynomial.linearSubstRep σ R n = { toFun := fun (M : (Matrix σ σ R)ᵐᵒᵖ) => (MvPolynomial.linearSubst (MulOpposite.unop M)).toLinearMap.restrict ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MvPolynomial.coe_linearSubstRep_apply {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] [DecidableEq σ] {n : ℕ} (M : (Matrix σ σ R)ᵐᵒᵖ) (p : ↥(homogeneousSubmodule σ R n)) : ↑(((linearSubstRep σ R n) M) p) = (linearSubst (MulOpposite.unop M)) ↑p