Enlarging the ambient affine space preserves the irreducible grid equation.
theorem
CCDN.irreducible_rename_of_injective
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
(i : σ → τ)
(hi : Function.Injective i)
(f : MvPolynomial σ K)
(hf : Irreducible f)
:
Irreducible ((MvPolynomial.rename i) f)
Renaming the variables of an irreducible polynomial along an injective map keeps it irreducible.
theorem
CCDN.totalDegree_rename_of_leftInverse
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[CommRing K]
(i : σ → τ)
(r : τ → σ)
(hr : Function.LeftInverse r i)
(f : MvPolynomial σ K)
:
Renaming the variables along a map with a left inverse preserves the total degree.
theorem
CCDN.exists_absolutely_irreducible_grid
{K : Type u_1}
{L : Type u_2}
[Field K]
[Infinite K]
[Field L]
(φ : K →+* L)
(s : Finset K)
(hs : 0 < s.card)
(d n : ℕ)
(hn : 2 ≤ n)
(hd : s.card + 2 ≤ d)
(hsize : 2 * s.card ≤ d + 1)
:
∃ (f : MvPolynomial (Fin n) K),
f.totalDegree = d ∧ Irreducible ((MvPolynomial.map φ) f) ∧ ∀ (z : Fin n → K), (∀ (i : Fin n), z i ∈ s) → (MvPolynomial.eval z) f = 0
The square-grid construction in any ambient dimension at least two. The added variables are free; irreducibility is preserved by polynomial extension.