Grace/Cumulus/Algebra/Field/PrincipalLocalization.g17

Open in Workbench Download source

Imports

Localization · Powers · Ring.Image

Declarations

Source

1-- Localizing at powers of a single nonzero element and clearing a common power.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.Field.PrincipalLocalization8import Localization9import Powers10import Ring.Image1112def denominatorPowers (B times unit s : Set) : Set :=13  {d ∈ B | ∃ n, Nat(n) ∧ d = monoidPow(times, unit, s, n)}1415notation scoped denominatorPowers(R, s) => denominatorPowers(R.carrier, R.mul, R.one, s)1617theorem denominatorPowers.one_mem (B times unit s : Set)18  requires oneIn : unit ∈ B19  shows unit ∈ denominatorPowers(B, times, unit, s)20proof21  have natural := Naturals.constructor.zero22  have value := monoidPow.zero at times, unit, s23  apply denominatorPowers.membership.backward24  refine ⟨oneIn, zero, natural, ?_⟩25  rw value26  rfl2728theorem monoidPow.in_subring (B plus z minus times unit T s : Set) (n : Nat)29  requires subring : IsSubring(B, plus, z, minus, times, unit, T)30  requires element : s ∈ T31  shows monoidPow(times, unit, s, n) ∈ T32proof33  induction n34  | zero =>35    rw monoidPow.zero36    exact IsSubring.one_closed with subring37  | succ(k) using ih =>38    have closed := IsSubring.mul_closed with subring39    rw monoidPow.succ40    exact ClosedBinary.mem with closed, element, ih4142section Powers43variable (B plus z minus times unit s y : Set)44notation ring S := (B, plus, z, minus, times, unit)45hypothesis ring : IsCommRing(S)46hypothesis inverse : IsInverse(B, times, unit, s, y)4748theorem IsInverse.powers (n : Nat)49  shows IsInverse(B, times, unit, monoidPow(S, s, n), monoidPow(S, y, n))50proof51  induction n52  | zero =>53    have ordinary := IsCommRing.ring with ring54    have monoid := IsRing.multiplicative with ordinary55    have oneIn := IsMonoid.unit_in_carrier with monoid56    have equation : S[1 * 1] = S[1] by ring57    rw monoidPow.zero58    rw monoidPow.zero59    unfold IsInverse60    refine ⟨oneIn, oneIn, equation, equation⟩61  | succ(k) using ih =>62    have ordinary := IsCommRing.ring with ring63    have monoid := IsRing.multiplicative with ordinary64    have data := inverse65    have inS := data.left66    have inY := data.right.left67    have inP := ih.left68    have inQ := ih.right.left69    have cancels := data.right.right.right70    have powersCancel := ih.right.right.right71    have productP := IsRing.mul_closed with ordinary, inS, inP72    have productQ := IsRing.mul_closed with ordinary, inY, inQ73    have right : S[(s * monoidPow(S, s, k)) * (y * monoidPow(S, y, k))] = S[1]74      have rearrange : S[(s * monoidPow(S, s, k)) * (y * monoidPow(S, y, k))] = S[(s * y) * (monoidPow(S, s, k) * monoidPow(S, y, k))]75        ring76      rw rearrange77      rw cancels78      rw powersCancel79      ring80    have left : S[(y * monoidPow(S, y, k)) * (s * monoidPow(S, s, k))] = S[1]81      have commute : S[(y * monoidPow(S, y, k)) * (s * monoidPow(S, s, k))] = S[(s * monoidPow(S, s, k)) * (y * monoidPow(S, y, k))]82        ring83      rw commute84      exact right85    rw monoidPow.succ86    rw monoidPow.succ87    unfold IsInverse88    refine ⟨productP, productQ, left, right⟩8990end Powers9192section Fields93variable (B plus z minus times unit T s : Set)94notation ring S := (B, plus, z, minus, times, unit)95hypothesis field : IsField(S)96hypothesis subring : IsSubring(S, T)97hypothesis element : s ∈ T98hypothesis nonzero : s ≠ S[0]99100theorem monoidPow.nonzero_in_field (n : Nat)101  shows monoidPow(S, s, n) ≠ S[0]102proof103  induction n104  | zero =>105    have distinct := IsField.nontrivial with field106    rw monoidPow.zero107    intro equal108    have reversed : S[0] = S[1] by cc109    exact distinct.right.right with reversed110  | succ(k) using ih =>111    have noZero := IsField.no_zero_divisors with field112    have ring := IsField.comm_ring with field113    have ordinary := IsCommRing.ring with ring114    have monoid := IsRing.multiplicative with ordinary115    have bound := IsSubring.subset_carrier with subring116    have sIn : s ∈ S by simp [Subset]117    have previous := monoidPow.closed at B, times, unit, s, k with *118    rw monoidPow.succ119    intro zeroProduct120    have alternatives := noZero with s, sIn, monoidPow(S, s, k), previous, zeroProduct121    cases alternatives with left | right122    . exact nonzero with left123    . exact ih with right124125theorem denominatorPowers.denominators126  shows Denominators(S, T, denominatorPowers(S, s))127proof128  have ring := IsField.comm_ring with field129  have ordinary := IsCommRing.ring with ring130  have monoid := IsRing.multiplicative with ordinary131  have bound := IsSubring.subset_carrier with subring132  have sIn : s ∈ S by simp [Subset]133  have oneIn := IsMonoid.unit_in_carrier with monoid134  have included : denominatorPowers(S, s) ⊆ T135    intros d hd136    obtain ⟨inD, n, natural, value⟩ := denominatorPowers.membership.forward with hd137    have member := monoidPow.in_subring with *138    rwa value139  have one : S[1] ∈ denominatorPowers(S, s)140    have natural := Naturals.constructor.zero141    have value := monoidPow.zero at times, unit, s142    apply denominatorPowers.membership.backward143    refine ⟨oneIn, zero, natural, ?_⟩144    rw value145    rfl146  have closed : ClosedBinary(denominatorPowers(S, s), times)147    intros x hx y hy148    obtain ⟨inX, m, naturalM, valueX⟩ := denominatorPowers.membership.forward with hx149    obtain ⟨inY, n, naturalN, valueY⟩ := denominatorPowers.membership.forward with hy150    have product := IsRing.mul_closed with ordinary, inX, inY151    have natural : Nat(add(m, n)) by typecheck152    have sum : monoidPow(S, s, add(m, n)) = S[monoidPow(S, s, m) * monoidPow(S, s, n)]153      exact monoidPow.add with *154    apply denominatorPowers.membership.backward155    refine ⟨product, add(m, n), natural, ?_⟩156    rw [valueX, valueY]157    cc158  have avoidsZero : ∀ d ∈ denominatorPowers(S, s), d ≠ S[0]159    intros d hd160    obtain ⟨inD, n, natural, value⟩ := denominatorPowers.membership.forward with hd161    have distinct := monoidPow.nonzero_in_field with *162    rwa value163  unfold Denominators164  refine ⟨included, one, closed, avoidsZero⟩165166theorem localizationWithin.clear_common_power (K : Set)167  requires finite : Finite(K)168  requires included : K ⊆ localizationWithin(S, T, denominatorPowers(S, s))169  shows ∃ n, Nat(n) ∧ (∀ x ∈ K, S[monoidPow(S, s, n) * x] ∈ T)170proof171  have ring := IsField.comm_ring with field172  have denominators := denominatorPowers.denominators with *173  obtain ⟨d, hd, clears⟩ := localizationWithin.clear_finite with ring, subring, denominators, finite, included174  obtain ⟨inD, n, natural, value⟩ := denominatorPowers.membership.forward with hd175  refine ⟨n, natural, ?_⟩176  intros x hx177  have member := clears with x, hx178  rwa value at member179180theorem localizationWithin.adjoin_single_inverse (y : Set)181  requires inverse : IsInverse(B, times, unit, s, y)182  shows localizationWithin(S, T, denominatorPowers(S, s)) = generatedSubring(S, insert(y, T))183proof184  have ring := IsField.comm_ring with field185  have denominators := denominatorPowers.denominators at B, plus, z, minus, times, unit, T, s with *186  have bound := IsSubring.subset_carrier with subring187  have yIn : y ∈ S by simp [IsInverse]188  have generatorsBound : insert(y, T) ⊆ S189    intros u hu190    simp [Subset, insert.membership]191  have generated := generatedSubring.subring at B, plus, z, minus, times, unit, insert(y, T) with *192  have contains := generatedSubring.contains with ring, generatorsBound193  have includesT : T ⊆ generatedSubring(S, insert(y, T))194    intros u hu195    have member := insert.contains at u, y, T with hu196    exact contains with u, member197  have containsY : y ∈ generatedSubring(S, insert(y, T))198    have member := insert.self at y, T199    exact contains with y, member200  have inverses : ∀ d ∈ denominatorPowers(S, s), ∃ v ∈ generatedSubring(S, insert(y, T)), IsInverse(B, times, unit, d, v)201    intros d hd202    obtain ⟨inD, n, natural, value⟩ := denominatorPowers.membership.forward with hd203    have member := monoidPow.in_subring at B, plus, z, minus, times, unit, generatedSubring(S, insert(y, T)), y, n with *204    have powers := IsInverse.powers at B, plus, z, minus, times, unit, s, y, n with *205    refine ⟨monoidPow(S, y, n), member, ?_⟩206    rwa value207  have first := localizationWithin.least with ring, subring, denominators, generated, includesT, inverses208  have localized := localizationWithin.subring with ring, subring, denominators209  have original := localizationWithin.contains with ring, subring, denominators210  have sIn : s ∈ S by simp [Subset]211  have sDenominator : s ∈ denominatorPowers(S, s)212    have natural := Naturals.constructor.succ with Naturals.constructor.zero213    have value : monoidPow(S, s, succ(zero)) = s214      rw [monoidPow.succ, monoidPow.zero]215      ring216    apply denominatorPowers.membership.backward217    refine ⟨sIn, succ(zero), natural, ?_⟩218    rw value219    rfl220  have localizedY := localizationWithin.inverse_mem with ring, subring, denominators, sDenominator, inverse221  have generators : insert(y, T) ⊆ localizationWithin(S, T, denominatorPowers(S, s))222    intros u hu223    have alternatives := insert.membership.forward with hu224    cases alternatives with equal | old225    . rw equal226      exact localizedY227      exact original with u, old228  have second := generatedSubring.least with ring, localized, generators229  exact Subset.antisymmetric with first, second230231end Fields232section Maps233variable (A add z neg mul one B plus o minus times unit f s : Set)234notation ring R := (A, add, z, neg, mul, one)235notation ring S := (B, plus, o, minus, times, unit)236hypothesis source : IsCommRing(R)237hypothesis target : IsCommRing(S)238hypothesis hom : IsRingHom(f, R, S)239hypothesis element : s ∈ R240241theorem IsRingHom.denominator_powers242  shows functionImage(f, denominatorPowers(R, s), S) = denominatorPowers(S, f(s))243proof244  have function := IsRingHom.function with hom245  have ordinary := IsCommRing.ring with source246  have monoid := IsRing.multiplicative with ordinary247  have bounded : denominatorPowers(R, s) ⊆ R by simp [Subset, denominatorPowers]248  ext d249  constructor250  . intro member251    obtain ⟨inS, a, inD, equal⟩ := functionImage.membership.forward with member252    obtain ⟨inA, n, natural, shape⟩ := denominatorPowers.membership.forward with inD253    have mapped := IsRingHom.power at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, s, n with *254    apply denominatorPowers.membership.backward255    refine ⟨inS, n, natural, ?_⟩256    cc257  . intro member258    obtain ⟨inS, n, natural, shape⟩ := denominatorPowers.membership.forward with member259    have power := monoidPow.closed with *260    have inD : monoidPow(R, s, n) ∈ denominatorPowers(R, s)261      apply denominatorPowers.membership.backward262      refine ⟨power, n, natural, ?_⟩263      rfl264    have mapped := IsRingHom.power at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, s, n with *265    apply functionImage.membership.backward266    refine ⟨inS, monoidPow(R, s, n), inD, ?_⟩267    cc268269theorem IsRingHom.principal_localization_subring270  requires field : IsField(S)271  requires injective : InjectiveBetween(f, R, S)272  requires nonzero : s ≠ R[0]273  shows IsSubring(S, localizationWithin(S, functionImage(f, R, S), functionImage(f, denominatorPowers(R, s), S)))274proof275  have image := IsRingHom.image_subring with *276  have function := IsRingHom.function with hom277  have member := functionImage.value with *278  have zeroIn : R[0] ∈ R by typecheck279  have zeroValue := IsRingHom.zero with hom280  have distinct : f(s) ≠ S[0]281    intro vanishes282    have equal : f(s) = f(R[0]) by cc283    have closed := FunctionBetween.apply_closed at f, A, B, s with *284    have first := FunctionBetween.relates_apply at f, A, B, s with *285    have second := FunctionBetween.relates_apply at f, A, B, z with *286    rw ← equal at second287    have impossible := Injective.cancel at f, A, B, s, z, f(s) with *288    exact nonzero with impossible289  have denominators := denominatorPowers.denominators with *290  have mapped := IsRingHom.denominator_powers at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, s with *291  rw mapped292  exact localizationWithin.subring with *293294end Maps295