English
For a finite set S of multivariate polynomials over a field K with compatible ring structure, the set of all coefficients of all monomials that appear in polynomials of S is definable in the ring language with respect to the zero locus of the span of S.
Русский
Для конечного множества S многочленов в полях K, над кольцом с совместимой структурой, множество всех коэффициентов всех мономов, встречающихся в полиномах из S, является определимым во языке колец относительно нулевого множества области, задаваемого образом span(S).
LaTeX
$$$ \\operatorname{Set.Definable}\\left( \\bigcup_{p \\in S} p.coeff'' p.support : \\operatorname{Set}K \\right)\\;\\text{Language.ring}\\left( \\operatorname{zeroLocus}(K, \\operatorname{Ideal.span}(S:\\text{ Set }(MvPolynomial ι K))) \\right). $$$
Lean4
theorem mvPolynomial_zeroLocus_definable {ι K : Type*} [Field K] [CompatibleRing K] (S : Finset (MvPolynomial ι K)) :
Set.Definable (⋃ p ∈ S, p.coeff '' p.support : Set K) Language.ring
(zeroLocus K (Ideal.span (S : Set (MvPolynomial ι K)))) :=
by
rw [Set.definable_iff_exists_formula_sum]
let p' := genericPolyMap (fun p : S => p.1.support)
letI := Classical.decEq ι
letI := Classical.decEq K
rw [MvPolynomial.zeroLocus_span]
refine
⟨BoundedFormula.iInf
(fun i : S =>
Term.equal
((termOfFreeCommRing (p' i)).relabel
(Sum.map
(fun p =>
⟨p.1.1.coeff p.2.1, by
simp only [Set.mem_iUnion]
exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩⟩)
id))
0),
?_⟩
simp [Formula.Realize, Term.equal, Function.comp_def, p', MvPolynomial.aeval_eq_eval₂Hom]
