-- Arbitrary nonzero polynomial denominators over infinite fields (ZF).
-- 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.InfiniteFieldLocalization
import Nonvanishing
import LocalizationObstruction
import Field.IntegralDescent

section Localizations
variable (I A add z neg mul one B plus o minus times unit g s j T : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring P := R[I]
notation ring S := (B, plus, o, minus, times, unit)
notation ring L := S ↾ T
hypothesis coefficients : IsField(R)
hypothesis infinite : ¬Finite(R)
hypothesis polynomial : s ∈ P
hypothesis nonzero : s ≠ P[0]
hypothesis index : j ∈ I
hypothesis embedding : IsRingHom(g, P, S)
hypothesis injective : InjectiveBetween(g, P, S)

theorem polynomialLocalization.not_field
  requires target : IsCommRing(S)
  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))
  shows ¬IsField(L)
proof
  obtain ⟨v, assignment, nonvanishing⟩ := polynomialAt.exists_nonzero at I, A, add, z, neg, mul, one, s with *
  exact polynomialLocalization.not_field_at_point with *

theorem polynomialLocalization.proper
  requires target : IsField(S)
  shows localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S)) ≠ S
proof
  obtain ⟨v, assignment, nonvanishing⟩ := polynomialAt.exists_nonzero at I, A, add, z, neg, mul, one, s with *
  exact polynomialLocalization.proper_at_point with *

theorem polynomialLocalization.not_integral
  requires target : IsField(S)
  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))
  shows ¬(∀ y ∈ S, IntegralOver(identity(T), L, S, y))
proof
  have ring := IsField.comm_ring with coefficients
  have source := polynomials.comm_ring at I, A, add, z, neg, mul, one with *
  have ambient := IsField.comm_ring with target
  have subring : IsSubring(S, T)
    rw carrier
    exact IsRingHom.principal_localization_subring with *
  have smaller := IsSubring.comm_ring with ambient, subring
  have inclusion := IsSubring.inclusion_hom with ambient, subring
  have faithful := IsSubring.inclusion_injective with subring
  have obstruction : ¬IsField(L)
    exact polynomialLocalization.not_field with *
  intro integral
  have descended : IsField(L)
    exact IsField.of_integral_extension with *
  exact obstruction with descended

theorem polynomialLocalization.exists_nonintegral
  requires target : IsField(S)
  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))
  shows ∃ y ∈ S, ¬IntegralOver(identity(T), L, S, y)
proof
  have obstruction : ¬(∀ y ∈ S, IntegralOver(identity(T), L, S, y))
    exact polynomialLocalization.not_integral with *
  by_contra absent
  apply obstruction
  intros y member
  by_contra nonintegral
  apply absent
  refine ⟨y, member, nonintegral⟩

end Localizations