Coefficient loci for roots in a compact set

For a compact subset S of a T₁ topological algebra, the monic polynomials of fixed degree having a root in S form a closed set in coefficient space. Thus their indicators are measurable whenever open sets are measurable. This applies in particular to compact valuation balls, whose root loci occur in finite decompositions of root-count integrals.

The proof uses joint continuity of evaluation and closedness of projection along a compact space. No separability or field hypothesis is needed.

theorem TauCeti.Polynomial.isClosed_setOf_exists_aeval_monicOfCoeff_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [IsTopologicalSemiring A] [T1Space A] (hφ : Continuous ⇑(algebraMap R A)) {S : Set A} (hS : IsCompact S) (n : ℕ) : IsClosed {a : Fin n → R | ∃ z ∈ S, (Polynomial.aeval z) (monicOfCoeff a) = 0}

The coefficient vectors of monic polynomials having a root in a fixed compact subset of a T₁ topological algebra form a closed set. The structure map is assumed continuous.