PolynomialLocalization

A nonvanishing evaluation point obstructs polynomial localization, in ZF

Open in Workbench View on GitHub

1-- A nonvanishing evaluation point obstructs polynomial localization, in ZF.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 PolynomialLocalization8import Grace.Cumulus.Algebra.Polynomial.LocalizationObstruction9import Grace.Cumulus.Algebra.Field.IntegralDescent1011section Embeddings12variable (I A add zero neg mul one B plus z minus times unit g v s j : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]15notation ring S := (B, plus, z, minus, times, unit)16hypothesis coefficients : IsField(R)17hypothesis field : IsField(S)18hypothesis embedding : IsRingHom(g, P, S)19hypothesis injective : InjectiveBetween(g, P, S)20hypothesis assignment : v : I → R21hypothesis polynomial : s ∈ P22hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]23hypothesis index : j ∈ I2425theorem cannot_exhaust_field26  shows localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S)) ≠ S27proof28  exact polynomialLocalization.proper_at_point with *2930end Embeddings31section Localizations32variable (I A add zero neg mul one B plus z minus times unit g v s j T : Set)33notation ring R := (A, add, zero, neg, mul, one)34notation ring P := R[I]35notation ring S := (B, plus, z, minus, times, unit)36hypothesis coefficients : IsField(R)37hypothesis target : IsCommRing(S)38hypothesis embedding : IsRingHom(g, P, S)39hypothesis injective : InjectiveBetween(g, P, S)40hypothesis assignment : v : I → R41hypothesis polynomial : s ∈ P42hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]43hypothesis index : j ∈ I4445notation ring L := S ↾ T46hypothesis carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))4748theorem not_a_field49  shows ¬IsField(L)50proof51  exact polynomialLocalization.not_field_at_point with *5253section IntegralExtensions54variable (C sum o inverse product e f : Set)55notation ring F := (C, sum, o, inverse, product, e)56hypothesis localRing : IsCommRing(L)57hypothesis field : IsField(F)58hypothesis hom : IsRingHom(f, L, F)59hypothesis faithful : InjectiveBetween(f, L, F)6061theorem cannot_have_integral_field_extension62  shows ¬(∀ y ∈ F, IntegralOver(f, L, F, y))63proof64  have obstruction : ¬IsField(L)65    exact polynomialLocalization.not_field_at_point with *66  intro integral67  have contradiction : IsField(L)68    exact IsField.of_integral_extension with *69  exact obstruction with contradiction7071end IntegralExtensions72end Localizations73