Grace/Cumulus/Algebra/Localization.g17

Open in Workbench Download source

Imports

Ring.GeneratedSubring · Field.Construction · Cardinal.ListSupport

Declarations

Source

1-- Localization inside an ambient commutative ring, with explicit denominators (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.Localization8import Ring.GeneratedSubring9import Field.Construction10import Cardinal.ListSupport1112predicate Denominators (B times z unit T D : Set) :=13  D ⊆ T ∧ unit ∈ D ∧ ClosedBinary(D, times) ∧ (∀ d ∈ D, d ≠ z)1415notation scoped Denominators(R, T, D) => Denominators(R.carrier, R.mul, R.zero, R.one, T, D)1617def localizationWithin (B times T D : Set) : Set :=18  {x ∈ B | ∃ d ∈ D, times(d, x) ∈ T}1920notation scoped localizationWithin(R, T, D) => localizationWithin(R.carrier, R.mul, T, D)2122theorem localizationWithin.subset (B times T D : Set)23  shows localizationWithin(B, times, T, D) ⊆ B24proof25  simp2627section Rings28variable (B plus z minus times unit T D : Set)29notation ring S := (B, plus, z, minus, times, unit)30hypothesis ring : IsCommRing(S)31hypothesis subring : IsSubring(S, T)32hypothesis denominators : Denominators(S, T, D)3334theorem Denominators.subset35  shows D ⊆ T36proof37  simp [Denominators]3839theorem Denominators.one_mem40  shows S[1] ∈ D41proof42  simp [Denominators]4344theorem Denominators.mul_closed45  shows ClosedBinary(D, times)46proof47  simp [Denominators]4849theorem Denominators.nonzero (d : Set)50  requires member : d ∈ D51  shows d ≠ S[0]52proof53  exact denominators.right.right.right with d, member5455theorem localizationWithin.contains56  shows T ⊆ localizationWithin(S, T, D)57proof58  have ordinary := IsCommRing.ring with ring59  have bounded := IsSubring.subset_carrier with subring60  have one := Denominators.one_mem with *61  intros x hx62  have inB : x ∈ S by simp [Subset]63  have equation : S[1 * x] = x by ring64  apply localizationWithin.membership.backward65  refine ⟨inB, unit, one, ?_⟩66  rwa equation6768theorem localizationWithin.subring69  shows IsSubring(S, localizationWithin(S, T, D))70proof71  have ordinary := IsCommRing.ring with ring72  have bounded := IsSubring.subset_carrier with subring73  have denomBound := Denominators.subset with *74  have denomClosed := Denominators.mul_closed with *75  have denomAmbient := Subset.transitive with denomBound, bounded76  have contains := localizationWithin.contains with *77  have subset := localizationWithin.subset at B, times, T, D78  have zero := IsSubring.zero_closed with subring79  have one := IsSubring.one_closed with subring80  have zeroMem : S[0] ∈ localizationWithin(S, T, D) by simp [Subset]81  have oneMem : S[1] ∈ localizationWithin(S, T, D) by simp [Subset]82  have negClosed := IsSubring.neg_closed with subring83  have addClosed := IsSubring.add_closed with subring84  have mulClosed := IsSubring.mul_closed with subring85  have negative : ClosedUnary(localizationWithin(S, T, D), minus)86    intros x hx87    obtain ⟨inB, d, hd, cleared⟩ := localizationWithin.membership.forward with hx88    have dIn : d ∈ S by simp [Subset]89    have closed := IsRing.neg_closed with ordinary, inB90    have numerator := ClosedUnary.mem with negClosed, cleared91    have equation : S[d * (-x)] = S[-(d * x)] by ring92    apply localizationWithin.membership.backward93    refine ⟨closed, d, hd, ?_⟩94    rwa equation95  have addition : ClosedBinary(localizationWithin(S, T, D), plus)96    intros x hx y hy97    obtain ⟨inX, d, hd, numeratorX⟩ := localizationWithin.membership.forward with hx98    obtain ⟨inY, e, he, numeratorY⟩ := localizationWithin.membership.forward with hy99    have dIn : d ∈ S by simp [Subset]100    have eIn : e ∈ S by simp [Subset]101    have dInT : d ∈ T by simp [Subset]102    have eInT : e ∈ T by simp [Subset]103    have denominator := ClosedBinary.mem with denomClosed, hd, he104    have left := ClosedBinary.mem with mulClosed, eInT, numeratorX105    have right := ClosedBinary.mem with mulClosed, dInT, numeratorY106    have numerator := ClosedBinary.mem with addClosed, left, right107    have closed := IsRing.add_closed with ordinary, inX, inY108    have equation : S[(d * e) * (x + y)] = S[e * (d * x) + d * (e * y)] by ring109    apply localizationWithin.membership.backward110    refine ⟨closed, S[d * e], denominator, ?_⟩111    rwa equation112  have multiplication : ClosedBinary(localizationWithin(S, T, D), times)113    intros x hx y hy114    obtain ⟨inX, d, hd, numeratorX⟩ := localizationWithin.membership.forward with hx115    obtain ⟨inY, e, he, numeratorY⟩ := localizationWithin.membership.forward with hy116    have dIn : d ∈ S by simp [Subset]117    have eIn : e ∈ S by simp [Subset]118    have denominator := ClosedBinary.mem with denomClosed, hd, he119    have numerator := ClosedBinary.mem with mulClosed, numeratorX, numeratorY120    have closed := IsRing.mul_closed with ordinary, inX, inY121    have equation : S[(d * e) * (x * y)] = S[(d * x) * (e * y)] by ring122    apply localizationWithin.membership.backward123    refine ⟨closed, S[d * e], denominator, ?_⟩124    rwa equation125  unfold IsSubring126  refine ⟨subset, zeroMem, oneMem, negative, addition, multiplication⟩127128theorem localizationWithin.inverse_mem (d y : Set)129  requires member : d ∈ D130  requires inverse : IsInverse(B, times, unit, d, y)131  shows y ∈ localizationWithin(S, T, D)132proof133  have one := IsSubring.one_closed with subring134  apply localizationWithin.membership.backward135  refine ⟨inverse.right.left, d, member, ?_⟩136  have cancels := inverse.right.right.right137  rwa cancels138139theorem localizationWithin.least (V : Set)140  requires larger : IsSubring(S, V)141  requires included : T ⊆ V142  requires inverses : ∀ d ∈ D, ∃ y ∈ V, IsInverse(B, times, unit, d, y)143  shows localizationWithin(S, T, D) ⊆ V144proof145  have bound := IsSubring.subset_carrier with subring146  have denomBound := Denominators.subset with *147  have ambient := Subset.transitive with denomBound, bound148  have closure := IsSubring.mul_closed with larger149  intros x hx150  obtain ⟨inX, d, hd, numerator⟩ := localizationWithin.membership.forward with hx151  obtain ⟨y, hy, inverse⟩ := inverses with d, hd152  have dIn : d ∈ S by simp [Subset]153  have inV : S[d * x] ∈ V by simp [Subset]154  have inY := inverse.right.left155  have cancels := inverse.right.right.left156  have member := ClosedBinary.mem with closure, hy, inV157  have equation : S[y * (d * x)] = x158    have associate : S[y * (d * x)] = S[(y * d) * x] by ring159    rw [associate, cancels]160    ring161  rwa equation at member162163end Rings164