Module

Nonvanishing.lean

Nyll.SchemeTheory.NoetherNormalization.Nonvanishing

3 declarations indexed from sourceView source ↗

Module documentation

Nonvanishing evaluations over infinite fields

This file supplies the nonvanishing step used in the constructive proof of Fried--Jarden, Lemma 22.5.1, and hence in the linear refinement of Proposition 6.2.1. The second theorem says that dehomogenizing a nonzero homogeneous polynomial by setting one coordinate equal to 1 remains nonzero.

Imports1

Mathlib.RingTheory.MvPolynomial.Homogeneous

Imported by2

theorem

exists_eval_ne_zero_fin

L31 ↗

FieldArithmetic.Chapter06.exists_eval_ne_zero_fin

Documentation

A nonzero multivariable polynomial in finitely many variables over an infinite field has a nonzero evaluation.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open Cardinal Polynomial
open MvPolynomial
variable {K : Type*} [Field K] [Infinite K]

Lean source · full declaration

theorem exists_eval_ne_zero_fin :
    ∀ {n : ℕ} {F : MvPolynomial (Fin n) K}, F ≠ 0 → ∃ r, eval r F ≠ 0
  | 0, F, hF => by
      use 0
      contrapose hF
      ext d
      simpa only [Subsingleton.elim d 0, MvPolynomial.eval_zero,
        AddMonoidAlgebra.coeff_zero] using! hF
  | n + 1, F, hF => by
      let p : Polynomial (MvPolynomial (Fin n) K) := finSuccEquiv K n F
      have hp : p ≠ 0 := EmbeddingLike.map_ne_zero_iff.2 hF
      obtain ⟨i, hi⟩ : ∃ i : ℕ, p.coeff i ≠ 0 := by
        contrapose! hp
        exact Polynomial.ext hp
      obtain ⟨r, hr⟩ := exists_eval_ne_zero_fin hi
      let q : K[X] := p.map (eval r)
      have hq : q ≠ 0 := by
        intro hq
        apply hr
        rw [← MvPolynomial.coeff_eval_eq_eval_coeff (Fin n) r p i]
        change q.coeff i = 0
        rw [hq, Polynomial.coeff_zero]
      have hqK : q.natDegree < #K :=
        lt_of_lt_of_le Cardinal.natCast_lt_aleph0
          (Cardinal.infinite_iff.mp ‹Infinite K›)
      obtain ⟨y, hy⟩ := q.exists_eval_ne_zero_of_natDegree_lt_card hq hqK
      use Fin.cons y r
      rwa [eval_eq_eval_mv_eval']

theorem

exists_eval_finCons_one_ne_zero

L67 ↗

FieldArithmetic.Chapter06.exists_eval_finCons_one_ne_zero

Documentation

If F is a nonzero homogeneous polynomial, then its first coordinate can be fixed to 1 while retaining a nonzero evaluation.

This is the dehomogenization argument behind the choice of the coefficients cᵢ in Fried--Jarden, Lemma 22.5.1.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open Cardinal Polynomial
open MvPolynomial
variable {K : Type*} [Field K] [Infinite K]

Lean source · statement

theorem exists_eval_finCons_one_ne_zero
    {n d : ℕ} {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F.IsHomogeneous d) (hF₀ : F ≠ 0) :
    ∃ r : Fin n → K, eval (Fin.cons 1 r) F ≠ 0

theorem

exists_eval_finSnoc_one_ne_zero

L134 ↗

FieldArithmetic.Chapter06.exists_eval_finSnoc_one_ne_zero

Documentation

The last-coordinate version of exists_eval_finCons_one_ne_zero, in the form used in Fried--Jarden's triangular change of variables.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open Cardinal Polynomial
open MvPolynomial
variable {K : Type*} [Field K] [Infinite K]

Lean source · statement

theorem exists_eval_finSnoc_one_ne_zero
    {n d : ℕ} {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F.IsHomogeneous d) (hF₀ : F ≠ 0) :
    ∃ r : Fin n → K, eval (Fin.snoc r 1) F ≠ 0

Module documentation

Nonvanishing evaluations over infinite fields

Declarations

exists_eval_ne_zero_fin

exists_eval_finCons_one_ne_zero

exists_eval_finSnoc_one_ne_zero