theorem Polynomial.exists_eval_ne_zero {k : Type u_1} [Field k] [Infinite k] {p : Polynomial k} (hp : p ≠ 0) : ∃ (a : k), eval a p ≠ 0

Over an infinite field, every nonzero univariate polynomial has a non-root (Lec 3, Lem 3 input).

theorem Polynomial.exists_not_isRoot {k : Type u_1} [Field k] [Infinite k] {p : Polynomial k} (hp : p ≠ 0) : ∃ (a : k), ¬p.IsRoot a

Over an infinite field, every nonzero polynomial has a non-root.

theorem Polynomial.eval_ne_zero_of_infinite {k : Type u_1} [Field k] [Infinite k] {p : Polynomial k} (hp : p ≠ 0) : ∃ (a : k), p.IsRoot a = False

Restatement: over an infinite field, some evaluation of a nonzero polynomial is False as a Prop for IsRoot.

theorem Polynomial.eval_eval_eq_eval_map_eval {k : Type u_1} [CommSemiring k] (p : Polynomial (Polynomial k)) (a b : k) : eval a (eval (C b) p) = eval b (map (evalRingHom a) p)

Iterated evaluation lemma: evaluating in the outer variable at C b and then the inner at a agrees with mapping by eval a and evaluating at b.

theorem exists_eval_ne_zero_bivariate {k : Type u_1} [Field k] [Infinite k] {p : Polynomial (Polynomial k)} (hp : p ≠ 0) : ∃ (a : k) (b : k), Polynomial.eval a (Polynomial.eval (Polynomial.C b) p) ≠ 0

Bivariate version: over an infinite field every nonzero polynomial in two variables has a non-zero evaluation.

theorem MvPolynomial.exists_eval_ne_zero {k : Type u_1} [Field k] [Infinite k] {σ : Type u_2} {f : MvPolynomial σ k} (hf : f ≠ 0) : ∃ (v : σ → k), (eval v) f ≠ 0

Lec 3, Lem 3: over an infinite field every nonzero polynomial in arbitrarily many variables has a non-vanishing evaluation.

theorem t1_comp_neg {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (c : k) : (NoetherNormalization.T1 f c).comp (NoetherNormalization.T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Composing the Nagata substitution with its negative inverse yields the identity.

@[reducible, inline]

noncomputable abbrev nagataEquiv {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] MvPolynomial (Fin (n + 1)) k

The Nagata change-of-variables k-algebra automorphism of k[x_0, …, x_n] used to make leading coefficients units (Lec 3, Lem 3).

theorem lt_up_of_mem {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v : Fin (n + 1) →₀ ℕ) (vlt : ∀ (i : Fin (n + 1)), v i < (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f) (l : ℕ) : l ∈ List.ofFn ⇑v → l < (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f

Helper: bounds on the digit values used in the Nagata substitution.

theorem sum_r_mul_ne {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v w : Fin (n + 1) →₀ ℕ) (vlt : ∀ (i : Fin (n + 1)), v i < (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f) (wlt : ∀ (i : Fin (n + 1)), w i < (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f) (hne : v ≠ w) : ∑ x : Fin (n + 1), (fun (f : MvPolynomial (Fin (n + 1)) k) (i : Fin (n + 1)) => (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f ^ ↑i) f x * v x ≠ ∑ x : Fin (n + 1), (fun (f : MvPolynomial (Fin (n + 1)) k) (i : Fin (n + 1)) => (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f ^ ↑i) f x * w x

Helper: distinct exponent vectors produce distinct weighted sums in the Nagata-substitution base-up f representation.

theorem degreeOf_zero_nagata {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v : Fin (n + 1) →₀ ℕ) {a : k} (ha : a ≠ 0) : MvPolynomial.degreeOf 0 ((nagataEquiv f) ((MvPolynomial.monomial v) a)) = ∑ i : Fin (n + 1), (fun (f : MvPolynomial (Fin (n + 1)) k) (i : Fin (n + 1)) => (fun (f : MvPolynomial (Fin (n + 1)) k) => 2 + f.totalDegree) f ^ ↑i) f i * v i

Helper: the degree in the first variable of a Nagata-transformed monomial equals the weighted sum of its exponents.

theorem degreeOf_ne_of_ne {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v w : Fin (n + 1) →₀ ℕ) (hv : v ∈ f.support) (hw : w ∈ f.support) (hne : v ≠ w) : MvPolynomial.degreeOf 0 ((nagataEquiv f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠ MvPolynomial.degreeOf 0 ((nagataEquiv f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))

Helper: distinct monomials in the support of f map under Nagata substitution to monomials with distinct degrees in the first variable.

theorem leadingCoeff_finSuccEquiv_nagata {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v : Fin (n + 1) →₀ ℕ) : ((MvPolynomial.finSuccEquiv k n) ((nagataEquiv f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff = (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Helper: the leading coefficient after Nagata transform of a single monomial equals the original coefficient (viewed in the inner ring).

theorem nagata_leadingcoeff_isUnit {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (fne : f ≠ 0) : IsUnit ((MvPolynomial.finSuccEquiv k n) ((nagataEquiv f) f)).leadingCoeff

Core of Lec 3, Lem 3: after the Nagata change of variables, the leading coefficient (in x_0) of f becomes a unit.

theorem MvPolynomial.exists_algEquiv_monic {k : Type u_1} [Field k] [Infinite k] {n : ℕ} (P : MvPolynomial (Fin (n + 1)) k) (hP : 0 < P.totalDegree) : ∃ (phi : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] MvPolynomial (Fin (n + 1)) k), IsUnit ((finSuccEquiv k n) (phi P)).leadingCoeff

Lec 3, Lem 3 (existence form): given a polynomial P of positive total degree, there is a k-algebra automorphism phi making the leading coefficient of phi P (as a polynomial in x_0) a unit.

theorem MvPolynomial.linear_change_of_variables_monic {k : Type u_1} [Field k] [Infinite k] {n : ℕ} (P : MvPolynomial (Fin (n + 1)) k) (hP : P ≠ 0) (hd : 0 < P.totalDegree) : ∃ (phi : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] MvPolynomial (Fin (n + 1)) k), ((finSuccEquiv k n) (phi P)).Monic ∧ ((finSuccEquiv k n) (phi P)).natDegree = P.totalDegree

Lec 3, Lem 3 (linear change of variables, monic form): there is a k-algebra automorphism phi after which phi P becomes monic in x_0 with degree equal to the total degree of P.