Sending every variable to the same single variable

The R-algebra map R[Xᵢ : i ∈ σ] → R[X] sending every variable Xᵢ to X is MvPolynomial.aeval fun _ => Polynomial.X. It is surjective as soon as σ is nonempty, and following it by X ↦ X_c is the renaming that sends every variable to X_c.

Main results

• MvPolynomial.rename_const_eq_aeval_aeval_X: renaming every variable to X_c factors through R[X].
• MvPolynomial.aeval_const_X_surjective: sending every variable to X is surjective onto R[X] when there is at least one variable.

theorem MvPolynomial.rename_const_eq_aeval_aeval_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (c : σ) (p : MvPolynomial σ R) : (rename fun (x : σ) => c) p = (Polynomial.aeval (X c)) ((aeval fun (x : σ) => Polynomial.X) p)

Renaming every variable to X_c is the map sending every variable to X, followed by X ↦ X_c.

theorem MvPolynomial.aeval_const_X_surjective (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Nonempty σ] : Function.Surjective ⇑(aeval fun (x : σ) => Polynomial.X)

Sending every variable to X is surjective onto R[X] when there is at least one variable.