Localization
Clearing coefficients in T[1/s] and an obstruction to finite module generation
1-- Clearing coefficients in T[1/s] and an obstruction to finite module generation.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Localization8import Grace.Cumulus.Algebra.Field.PrincipalLocalization910section Coefficients11variable (B plus z minus times unit T s y : Set)12notation ring S := (B, plus, z, minus, times, unit)13hypothesis field : IsField(S)14hypothesis subring : IsSubring(S, T)15hypothesis element : s ∈ T16hypothesis nonzero : s ≠ S[0]17hypothesis inverse : IsInverse(B, times, unit, s, y)1819theorem clear_coefficients (cs : List(B))20 requires coefficients : listSupport{B}(cs) ⊆ generatedSubring(S, insert(y, T))21 shows ∃ n, Nat(n) ∧ (∀ a ∈ listSupport{B}(cs), S[monoidPow(S, s, n) * a] ∈ T)22proof23 have finite := listSupport.finite at B, cs with *24 have localization := localizationWithin.adjoin_single_inverse at B, plus, z, minus, times, unit, T, s, y with *25 rw ← localization at coefficients26 exact localizationWithin.clear_common_power with field, subring, element, nonzero, finite, coefficients2728end Coefficients2930section Obstruction31variable (A add zero neg mul one B plus z minus times unit f T D : Set)32notation ring R := (A, add, zero, neg, mul, one)33notation ring S := (B, plus, z, minus, times, unit)34hypothesis source : IsCommRing(R)35hypothesis field : IsField(S)36hypothesis hom : IsRingHom(f, R, S)37hypothesis subalgebra : Subalgebra(f, R, S, T)38hypothesis denominators : Denominators(S, T, D)3940theorem proper_fraction_field_is_not_module_finite41 requires proper : T ≠ S42 requires fractions : localizationWithin(S, T, D) = S43 shows ¬FiniteAlgebraModule(f, R, S)44proof45 intro finite46 have equal := localizationWithin.eq_field_of_finite_module with source, field, hom, subalgebra, denominators, finite, fractions47 exact proper with equal4849end Obstruction50