-- Evaluation obstructs polynomial localization at a denominator nonvanishing at a point.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Polynomial.LocalizationObstruction
import PointIdeal
import Field.LocalizationObstruction
import Field.PrincipalLocalization

section Evaluation
variable (I A add zero neg mul one v s : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
hypothesis field : IsField(R)
hypothesis assignment : v : I → R
hypothesis polynomial : s ∈ P
hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]

theorem polynomialAt.denominator_powers_nonzero
  shows ∀ d ∈ denominatorPowers(P, s), polynomialAt(I, R, v)(d) ≠ R[0]
proof
  have ring := IsField.comm_ring with field
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have evaluation := polynomialAt.hom with *
  have valueIn := IsRingHom.closed with evaluation, polynomial
  intros d hd
  obtain ⟨member, n, natural, equal⟩ := denominatorPowers.membership.forward with hd
  have mapped : polynomialAt(I, R, v)(monoidPow(P, s, n)) = monoidPow(R, polynomialAt(I, R, v)(s), n)
    exact IsRingHom.power with *
  have nonzero : monoidPow(R, polynomialAt(I, R, v)(s), n) ≠ R[0]
    exact IsField.power_nonzero with *
  rwa [equal, mapped]

end Evaluation

section Embeddings
variable (I A add zero neg mul one B plus z minus times unit g v s j : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring S := (B, plus, z, minus, times, unit)
hypothesis coefficients : IsField(R)
hypothesis field : IsField(S)
hypothesis embedding : IsRingHom(g, P, S)
hypothesis injective : InjectiveBetween(g, P, S)
hypothesis assignment : v : I → R
hypothesis polynomial : s ∈ P
hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]
hypothesis index : j ∈ I

theorem polynomialLocalization.proper_at_point
  shows localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S)) ≠ S
proof
  have ring := IsField.comm_ring with coefficients
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have evaluation := polynomialAt.hom with *
  have bounded : denominatorPowers(P, s) ⊆ P by simp [Subset, denominatorPowers]
  have avoids := polynomialAt.denominator_powers_nonzero with *
  have coefficient := FunctionBetween.apply_closed with assignment, index
  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, v(j) with *
  have nontrivial := IsField.nontrivial with coefficients
  have distinct := Nontrivial.distinct with nontrivial
  have nonzero := polynomialCoordinateDifference.nonzero with distinct, index, coefficient
  have evaluated := polynomialAt.coordinate_difference with *
  have vanishes : polynomialAt(I, R, v)(polynomialCoordinateDifference(I, R, j, v(j))) = R[0]
    rw evaluated
    ring
  exact localizationWithin.proper_of_kernel with source, field, ring, embedding, injective, evaluation, bounded, avoids, member, nonzero, vanishes

end Embeddings
section Localizations
variable (I A add zero neg mul one B plus z minus times unit g v s j T : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring S := (B, plus, z, minus, times, unit)
hypothesis coefficients : IsField(R)
hypothesis target : IsCommRing(S)
hypothesis embedding : IsRingHom(g, P, S)
hypothesis injective : InjectiveBetween(g, P, S)
hypothesis assignment : v : I → R
hypothesis polynomial : s ∈ P
hypothesis nonvanishing : polynomialAt(I, R, v)(s) ≠ R[0]
hypothesis index : j ∈ I

notation ring L := S ↾ T
hypothesis carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))

theorem polynomialLocalization.not_field_at_point
  shows ¬IsField(L)
proof
  have ring := IsField.comm_ring with coefficients
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have evaluation := polynomialAt.hom with *
  have bounded : denominatorPowers(P, s) ⊆ P by simp [Subset, denominatorPowers]
  have avoids := polynomialAt.denominator_powers_nonzero with *
  have coefficient := FunctionBetween.apply_closed with assignment, index
  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, v(j) with *
  have nontrivial := IsField.nontrivial with coefficients
  have distinct := Nontrivial.distinct with nontrivial
  have nonzero := polynomialCoordinateDifference.nonzero with distinct, index, coefficient
  have evaluated := polynomialAt.coordinate_difference with *
  have vanishes : polynomialAt(I, R, v)(polynomialCoordinateDifference(I, R, j, v(j))) = R[0]
    rw evaluated
    ring
  have ordinary := IsCommRing.ring with source
  have monoid := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have denominatorOne := denominatorPowers.one_mem at P, polynomialMul(I, A, add, zero, neg, mul, one), P[1], s with oneIn
  exact localizationWithin.not_field_of_kernel with source, target, ring, embedding, injective, evaluation, bounded, avoids, denominatorOne, carrier, member, nonzero, vanishes

end Localizations