Grace/Cumulus/Algebra/Polynomial/HornerLocalization.g17
Imports
HornerPolynomial · LocalizationObstruction
Declarations
Source
1-- Localization at a nonzero-leading Horner polynomial is not a field, without a point hypothesis.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.HornerLocalization8import HornerPolynomial9import LocalizationObstruction1011section Localizations12variable (I A add z neg mul one B plus o minus times unit g j leading T : Set)13notation ring R := (A, add, z, neg, mul, one)14notation ring P := R[I]15notation ring S := (B, plus, o, minus, times, unit)16notation ring L := S ↾ T17hypothesis coefficients : IsField(R)18hypothesis infinite : ¬Finite(R)19hypothesis initial : leading ∈ R20hypothesis nonzero : leading ≠ R[0]21hypothesis index : j ∈ I22hypothesis target : IsCommRing(S)23hypothesis embedding : IsRingHom(g, P, S)24hypothesis injective : InjectiveBetween(g, P, S)2526theorem polynomialLocalization.not_field_from_horner (cs : List(A))27 requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, polynomialFromHorner(I, R, j, leading, cs)), S))28 shows ¬IsField(L)29proof30 have point : ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]31 exact polynomialFromHorner.nonvanishing with *32 obtain ⟨v, assignment, nonvanishing⟩ := point33 have ring := IsField.comm_ring with coefficients34 have polynomial : polynomialFromHorner(I, R, j, leading, cs) ∈ P35 exact polynomialFromHorner.member with *36 exact polynomialLocalization.not_field_at_point with *3738end Localizations39