PolynomialAvoidance.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-root and countable polynomial avoidance over the complex numbers

theorem OAI.Nagata.Workers.W25.exists_countable_nonzero_eval_fin line 23

Source documentation

A countable family of nonzero polynomials in finitely many variables has a simultaneous nonvanishing point over every uncountable integral domain.

theorem exists_countable_nonzero_eval_fin (K : Type*) [CommRing K] [IsDomain K]
    [Uncountable K] (n : ℕ) {ι : Type*} [Countable ι] :
    ∀ p : ι → MvPolynomial (Fin n) K, (∀ i, p i ≠ 0) →
      ∃ x : Fin n → K, ∀ i, eval x (p i) ≠ 0 := by
…

theorem OAI.Nagata.Workers.W25.exists_countable_nonzero_eval line 79

Source documentation

Coordinate-type-independent form of direct countable polynomial avoidance.

theorem exists_countable_nonzero_eval (K : Type*) [CommRing K] [IsDomain K]
    [Uncountable K] {σ ι : Type*} [Fintype σ] [Countable ι]
    (p : ι → MvPolynomial σ K) (hp : ∀ i, p i ≠ 0) :
    ∃ x : σ → K, ∀ i, eval x (p i) ≠ 0 := by
…

theorem OAI.Nagata.Workers.W25.exists_complex_polynomial_avoidance_direct line 106
Source documentation
A countable family of nonzero complex polynomials in finitely many variables has a simultaneous nonvanishing complex point. This proof uses finite root sets.
```
theorem exists_complex_polynomial_avoidance_direct {σ ι : Type*} [Fintype σ] [Countable ι]
    (p : ι → MvPolynomial σ ℂ) (hp : ∀ i, p i ≠ 0) :
    ∃ x : σ → ℂ, ∀ i, MvPolynomial.eval x (p i) ≠ 0 := by
…
```

theorem OAI.Nagata.Workers.W25.exists_distinct_affine_avoidance line 128

Source documentation

A countable family of nonzero affine equations admits a simultaneous avoiding tuple whose first coordinates are pairwise distinct.

theorem exists_distinct_affine_avoidance {r : ℕ} {ι : Type*} [Countable ι]
    (p : ι → MvPolynomial (Fin r × Fin 2) ℂ) (hp : ∀ i, p i ≠ 0) :
    ∃ x : Fin r × Fin 2 → ℂ,
      (∀ i, MvPolynomial.eval x (p i) ≠ 0) ∧
      Function.Injective (fun i : Fin r => x (i, 0)) := by
…

theorem OAI.Nagata.Workers.W25.exists_projective_affine_avoidance line 154

Source documentation

The affine avoiding tuple defines actual pairwise distinct projective points.

theorem exists_projective_affine_avoidance {r : ℕ} {ι : Type*} [Countable ι]
    (p : ι → MvPolynomial (Fin r × Fin 2) ℂ) (hp : ∀ i, p i ≠ 0) :
    ∃ (x : Fin r × Fin 2 → ℂ) (P : OrderedDistinctPoints r),
      (∀ i, P.val i = affinePlanePoint (fun j => x (i, j))) ∧
      (∀ i, MvPolynomial.eval x (p i) ≠ 0) := by
…

theorem OAI.Nagata.Workers.W25.complex_polynomial_funext line 179

Source documentation

Complex polynomials in finitely many variables agree if all evaluations agree.

theorem complex_polynomial_funext {σ : Type*} [Fintype σ]
    {p q : MvPolynomial σ ℂ}
    (h : ∀ x : σ → ℂ, MvPolynomial.eval x p = MvPolynomial.eval x q) : p = q := by
…