Grace/Cumulus/Algebra/Polynomial/LocalizationObstruction.g17

Open in Workbench Download source

Imports

PointIdeal · Field.LocalizationObstruction · Field.PrincipalLocalization

Declarations

Source

1-- Evaluation obstructs polynomial localization at a denominator nonvanishing at a point.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.LocalizationObstruction8import PointIdeal9import Field.LocalizationObstruction10import Field.PrincipalLocalization1112section Evaluation13variable (I A add zero neg mul one v s : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring P := R[I]16hypothesis field : IsField(R)17hypothesis assignment : v : I → R18hypothesis polynomial : s ∈ P19hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]2021theorem polynomialAt.denominator_powers_nonzero22  shows ∀ d ∈ denominatorPowers(P, s), polynomialAt(I, R, v)(d) ≠ R[0]23proof24  have ring := IsField.comm_ring with field25  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *26  have evaluation := polynomialAt.hom with *27  have valueIn := IsRingHom.closed with evaluation, polynomial28  intros d hd29  obtain ⟨member, n, natural, equal⟩ := denominatorPowers.membership.forward with hd30  have mapped : polynomialAt(I, R, v)(monoidPow(P, s, n)) = monoidPow(R, polynomialAt(I, R, v)(s), n)31    exact IsRingHom.power with *32  have nonzero : monoidPow(R, polynomialAt(I, R, v)(s), n) ≠ R[0]33    exact IsField.power_nonzero with *34  rwa [equal, mapped]3536end Evaluation3738section Embeddings39variable (I A add zero neg mul one B plus z minus times unit g v s j : Set)40notation ring R := (A, add, zero, neg, mul, one)41notation ring P := R[I]42notation ring S := (B, plus, z, minus, times, unit)43hypothesis coefficients : IsField(R)44hypothesis field : IsField(S)45hypothesis embedding : IsRingHom(g, P, S)46hypothesis injective : InjectiveBetween(g, P, S)47hypothesis assignment : v : I → R48hypothesis polynomial : s ∈ P49hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]50hypothesis index : j ∈ I5152theorem polynomialLocalization.proper_at_point53  shows localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S)) ≠ S54proof55  have ring := IsField.comm_ring with coefficients56  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *57  have evaluation := polynomialAt.hom with *58  have bounded : denominatorPowers(P, s) ⊆ P by simp [Subset, denominatorPowers]59  have avoids := polynomialAt.denominator_powers_nonzero with *60  have coefficient := FunctionBetween.apply_closed with assignment, index61  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, v(j) with *62  have nontrivial := IsField.nontrivial with coefficients63  have distinct := Nontrivial.distinct with nontrivial64  have nonzero := polynomialCoordinateDifference.nonzero with distinct, index, coefficient65  have evaluated := polynomialAt.coordinate_difference with *66  have vanishes : polynomialAt(I, R, v)(polynomialCoordinateDifference(I, R, j, v(j))) = R[0]67    rw evaluated68    ring69  exact localizationWithin.proper_of_kernel with source, field, ring, embedding, injective, evaluation, bounded, avoids, member, nonzero, vanishes7071end Embeddings72section Localizations73variable (I A add zero neg mul one B plus z minus times unit g v s j T : Set)74notation ring R := (A, add, zero, neg, mul, one)75notation ring P := R[I]76notation ring S := (B, plus, z, minus, times, unit)77hypothesis coefficients : IsField(R)78hypothesis target : IsCommRing(S)79hypothesis embedding : IsRingHom(g, P, S)80hypothesis injective : InjectiveBetween(g, P, S)81hypothesis assignment : v : I → R82hypothesis polynomial : s ∈ P83hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]84hypothesis index : j ∈ I8586notation ring L := S ↾ T87hypothesis carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))8889theorem polynomialLocalization.not_field_at_point90  shows ¬IsField(L)91proof92  have ring := IsField.comm_ring with coefficients93  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *94  have evaluation := polynomialAt.hom with *95  have bounded : denominatorPowers(P, s) ⊆ P by simp [Subset, denominatorPowers]96  have avoids := polynomialAt.denominator_powers_nonzero with *97  have coefficient := FunctionBetween.apply_closed with assignment, index98  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, v(j) with *99  have nontrivial := IsField.nontrivial with coefficients100  have distinct := Nontrivial.distinct with nontrivial101  have nonzero := polynomialCoordinateDifference.nonzero with distinct, index, coefficient102  have evaluated := polynomialAt.coordinate_difference with *103  have vanishes : polynomialAt(I, R, v)(polynomialCoordinateDifference(I, R, j, v(j))) = R[0]104    rw evaluated105    ring106  have ordinary := IsCommRing.ring with source107  have monoid := IsRing.multiplicative with ordinary108  have oneIn := IsMonoid.unit_in_carrier with monoid109  have denominatorOne := denominatorPowers.one_mem at P, polynomialMul(I, A, add, zero, neg, mul, one), P[1], s with oneIn110  exact localizationWithin.not_field_of_kernel with source, target, ring, embedding, injective, evaluation, bounded, avoids, denominatorOne, carrier, member, nonzero, vanishes111112end Localizations113