Maps out of a polynomial ring

An A-algebra homomorphism out of a polynomial ring A[X_σ] is determined freely by the images of the variables: MvPolynomial.aevalEquiv identifies such homomorphisms to S with the functions σ → S, the points of affine space. So a homomorphism lifts along every surjective A-algebra homomorphism f : R → S: send each variable to a preimage under f of its image.

Main results

• MvPolynomial.aevalEquiv: evaluation MvPolynomial.aeval is a bijection from σ → S onto A[X_σ] →ₐ[A] S, with inverse evaluation at the variables.
• MvPolynomial.exists_comp_eq_of_surjective: every g : A[X_σ] →ₐ[A] S factors as f.comp g' through any surjective f : R →ₐ[A] S.

noncomputable def MvPolynomial.aevalEquiv (σ : Type u_1) (A : Type u_2) (S : Type u_3) [CommSemiring A] [CommSemiring S] [Algebra A S] : (σ → S) ≃ (MvPolynomial σ A →ₐ[A] S)

Maps out of a polynomial ring are their values on the variables: MvPolynomial.aeval is a bijection from σ → S onto the A-algebra homomorphisms A[X_σ] →ₐ[A] S, with inverse evaluation at the variables.

@[simp]

theorem MvPolynomial.aevalEquiv_apply {σ : Type u_1} {A : Type u_2} {S : Type u_3} [CommSemiring A] [CommSemiring S] [Algebra A S] (v : σ → S) : (aevalEquiv σ A S) v = aeval v

@[simp]

theorem MvPolynomial.aevalEquiv_symm_apply {σ : Type u_1} {A : Type u_2} {S : Type u_3} [CommSemiring A] [CommSemiring S] [Algebra A S] (g : MvPolynomial σ A →ₐ[A] S) (i : σ) : (aevalEquiv σ A S).symm g i = g (X i)

theorem MvPolynomial.exists_comp_eq_of_surjective {σ : Type u_1} {A : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring A] [CommSemiring R] [CommSemiring S] [Algebra A R] [Algebra A S] {f : R →ₐ[A] S} (hf : Function.Surjective ⇑f) (g : MvPolynomial σ A →ₐ[A] S) : ∃ (g' : MvPolynomial σ A →ₐ[A] R), f.comp g' = g

Maps out of a polynomial ring lift along surjections: every A-algebra homomorphism g : A[X_σ] →ₐ[A] S factors as f.comp g' through any surjective f : R →ₐ[A] S.