Radial scaling X j ↦ X j * T of a multivariate polynomial; the coefficient of T ^ n is the homogeneous component of degree n.

noncomputable def CCDN.radialMap {K : Type u_1} {σ : Type u_2} [CommRing K] : MvPolynomial σ K →+* Polynomial (MvPolynomial σ K)

Replace every coordinate by itself times the same scalar parameter.

Equations

• CCDN.radialMap = MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun (j : σ) => Polynomial.C (MvPolynomial.X j) * Polynomial.X

@[simp]

theorem CCDN.radialMap_C {K : Type u_1} {σ : Type u_2} [CommRing K] (c : K) : radialMap (MvPolynomial.C c) = Polynomial.C (MvPolynomial.C c)

The radial map sends a constant C c to the constant polynomial C (C c).

@[simp]

theorem CCDN.radialMap_X {K : Type u_1} {σ : Type u_2} [CommRing K] (j : σ) : radialMap (MvPolynomial.X j) = Polynomial.C (MvPolynomial.X j) * Polynomial.X

The radial map sends the variable X j to X j * T.

theorem CCDN.radialMap_coeff {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (n : ℕ) : (radialMap f).coeff n = (MvPolynomial.homogeneousComponent n) f

The coefficient of T ^ n in the radial image of f is the homogeneous component of f of degree n.

theorem CCDN.radialMap_injective {K : Type u_1} {σ : Type u_2} [CommRing K] : Function.Injective ⇑radialMap

The radial map is injective, since evaluating at T = 1 recovers the polynomial.

theorem CCDN.constantCoeff_comp_radialMap {K : Type u_1} {σ : Type u_2} [CommRing K] : Polynomial.constantCoeff.comp radialMap = MvPolynomial.C.comp (MvPolynomial.eval fun (x : σ) => 0)

The constant coefficient of the radial image of f is the constant f(0).