Grace/Cumulus/Algebra/Polynomial/InfiniteFieldLocalization.g17

Open in Workbench Download source

Imports

Nonvanishing · LocalizationObstruction · Field.IntegralDescent

Declarations

Source

1-- Arbitrary nonzero polynomial denominators over infinite fields (ZF).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.InfiniteFieldLocalization8import Nonvanishing9import LocalizationObstruction10import Field.IntegralDescent1112section Localizations13variable (I A add z neg mul one B plus o minus times unit g s j T : Set)14notation ring R := (A, add, z, neg, mul, one)15notation ring P := R[I]16notation ring S := (B, plus, o, minus, times, unit)17notation ring L := S ↾ T18hypothesis coefficients : IsField(R)19hypothesis infinite : ¬Finite(R)20hypothesis polynomial : s ∈ P21hypothesis nonzero : s ≠ P[0]22hypothesis index : j ∈ I23hypothesis embedding : IsRingHom(g, P, S)24hypothesis injective : InjectiveBetween(g, P, S)2526theorem polynomialLocalization.not_field27  requires target : IsCommRing(S)28  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))29  shows ¬IsField(L)30proof31  obtain ⟨v, assignment, nonvanishing⟩ := polynomialAt.exists_nonzero at I, A, add, z, neg, mul, one, s with *32  exact polynomialLocalization.not_field_at_point with *3334theorem polynomialLocalization.proper35  requires target : IsField(S)36  shows localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S)) ≠ S37proof38  obtain ⟨v, assignment, nonvanishing⟩ := polynomialAt.exists_nonzero at I, A, add, z, neg, mul, one, s with *39  exact polynomialLocalization.proper_at_point with *4041theorem polynomialLocalization.not_integral42  requires target : IsField(S)43  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))44  shows ¬(∀ y ∈ S, IntegralOver(identity(T), L, S, y))45proof46  have ring := IsField.comm_ring with coefficients47  have source := polynomials.comm_ring at I, A, add, z, neg, mul, one with *48  have ambient := IsField.comm_ring with target49  have subring : IsSubring(S, T)50    rw carrier51    exact IsRingHom.principal_localization_subring with *52  have smaller := IsSubring.comm_ring with ambient, subring53  have inclusion := IsSubring.inclusion_hom with ambient, subring54  have faithful := IsSubring.inclusion_injective with subring55  have obstruction : ¬IsField(L)56    exact polynomialLocalization.not_field with *57  intro integral58  have descended : IsField(L)59    exact IsField.of_integral_extension with *60  exact obstruction with descended6162theorem polynomialLocalization.exists_nonintegral63  requires target : IsField(S)64  requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, s), S))65  shows ∃ y ∈ S, ¬IntegralOver(identity(T), L, S, y)66proof67  have obstruction : ¬(∀ y ∈ S, IntegralOver(identity(T), L, S, y))68    exact polynomialLocalization.not_integral with *69  by_contra absent70  apply obstruction71  intros y member72  by_contra nonintegral73  apply absent74  refine ⟨y, member, nonintegral⟩7576end Localizations77