PolynomialNonvanishing
Sparse polynomials over infinite fields and the localization obstruction
1-- Sparse polynomials over infinite fields and the localization obstruction.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialNonvanishing8import Grace.Cumulus.Algebra.Polynomial.InfiniteFieldLocalization910section Polynomials11variable (I A add z neg mul one : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring P := R[I]14hypothesis field : IsField(R)15hypothesis infinite : ¬Finite(R)1617-- No finiteness or nonemptiness assumption on I is needed here.18theorem nonvanishing (p : Set)19 requires polynomial : p ∈ P20 requires nonzero : p ≠ P[0]21 shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(p) ≠ z22proof23 exact polynomialAt.exists_nonzero with *2425theorem determined_by_values (p q : Set)26 requires left : p ∈ P27 requires right : q ∈ P28 requires agreement : ∀ v, FunctionBetween(v, I, R) → polynomialAt(I, R, v)(p) = polynomialAt(I, R, v)(q)29 shows p = q30proof31 exact polynomialAt.ext with *3233end Polynomials3435section Localizations36variable (I A add z neg mul one B plus o minus times unit g s j T : Set)37notation ring R := (A, add, z, neg, mul, one)38notation ring P := R[I]39notation ring S := (B, plus, o, minus, times, unit)40notation ring L := S ↾ T41hypothesis coefficients : IsField(R)42hypothesis infinite : ¬Finite(R)43hypothesis polynomial : s ∈ P44hypothesis nonzero : s ≠ P[0]45hypothesis index : j ∈ I46hypothesis embedding : IsRingHom(g, P, S)47hypothesis injective : InjectiveBetween(g, P, S)48hypothesis carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))4950theorem localization_not_field51 requires target : IsCommRing(S)52 shows ¬IsField(L)53proof54 exact polynomialLocalization.not_field with *5556theorem nonintegral_element57 requires target : IsField(S)58 shows ∃ y ∈ S, ¬IntegralOver(identity(T), L, S, y)59proof60 exact polynomialLocalization.exists_nonintegral with *6162end Localizations63