Scalar extension commutes with a polynomial image ideal. Consequently a polynomial projection of a geometrically integral source has a geometrically integral image.

theorem CCDN.polynomialCoefficientLinear_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m n : ℕ} (φ : L →ₗ[K] K) (a : Fin m → MvPolynomial (Fin n) K) (g : MvPolynomial (Fin m) L) : (polynomialCoefficientLinear φ) ((MvPolynomial.aeval fun (i : Fin m) => (MvPolynomial.map (algebraMap K L)) (a i)) g) = (MvPolynomial.aeval a) ((polynomialCoefficientLinear φ) g)

Coefficient functionals commute with substitution of polynomials defined over the base field, even though they need not preserve multiplication.

theorem CCDN.mem_projectionCoordinateMap_ker {K : Type u_1} [Field K] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (a : Fin m → MvPolynomial (Fin n) K) (f : MvPolynomial (Fin m) K) : f ∈ RingHom.ker (projectionCoordinateMap I a) ↔ (MvPolynomial.aeval a) f ∈ I

A polynomial f lies in the kernel of the coordinate map Y i ↦ a i into MvPolynomial (Fin n) K ⧸ I if and only if the substitution aeval a f lies in I.

theorem CCDN.projection_kernel_scalar_extension {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (a : Fin m → MvPolynomial (Fin n) K) : Ideal.map (MvPolynomial.map (algebraMap K L)) (RingHom.ker (projectionCoordinateMap I a)) = RingHom.ker (projectionCoordinateMap (Ideal.map (MvPolynomial.map (algebraMap K L)) I) fun (i : Fin m) => (MvPolynomial.map (algebraMap K L)) (a i))

The scalar-extended image ideal is the image ideal of the scalar-extended source. The substitution need not be linear, finite or birational.

theorem CCDN.projection_kernel_geometrically_prime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [(Ideal.map (MvPolynomial.map (algebraMap K L)) I).IsPrime] (a : Fin m → MvPolynomial (Fin n) K) : (Ideal.map (MvPolynomial.map (algebraMap K L)) (RingHom.ker (projectionCoordinateMap I a))).IsPrime

If the ideal I stays prime after extending scalars from K to L, then so does the kernel of the coordinate map Y i ↦ a i into MvPolynomial (Fin n) K ⧸ I, that is, the ideal of the image of the polynomial map a.

theorem CCDN.projection_equation_irreducible_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [(Ideal.map (MvPolynomial.map (algebraMap K L)) I).IsPrime] (a : Fin m → MvPolynomial (Fin n) K) (f : MvPolynomial (Fin m) K) (hf : f ≠ 0) (hker : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}) : Irreducible ((MvPolynomial.map (algebraMap K L)) f)

A nonzero equation generating the image ideal remains irreducible over every field extension where the source ideal stays prime.