Grace/Cumulus/Algebra/ClearDenominators.g17

Open in Workbench Download source

Imports

Localization · FiniteSpan

Declarations

Source

1-- One common denominator for finite sets and finitely spanned submodules (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.ClearDenominators8import Localization9import FiniteSpan1011section Rings12variable (B plus z minus times unit T D : Set)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis ring : IsCommRing(S)15hypothesis subring : IsSubring(S, T)16hypothesis denominators : Denominators(S, T, D)1718theorem localizationWithin.clear_list (K : Set) (xs : List(K))19  requires included : K ⊆ localizationWithin(S, T, D)20  shows ∃ d ∈ D, ∀ x ∈ listSupport{K}(xs), S[d * x] ∈ T21proof22  induction xs23  | List.nil =>24    have one := Denominators.one_mem with ring, subring, denominators25    refine ⟨unit, one, ?_⟩26    intros x hx27    rw listSupport at hx28    exfalso29    exact set.empty with hx30  | List.cons(x, tail) using ih =>31    have bounded := IsSubring.subset_carrier with subring32    have denomBound := Denominators.subset with ring, subring, denominators33    have denomAmbient := Subset.transitive with denomBound, bounded34    have denomClosed := Denominators.mul_closed with ring, subring, denominators35    have multiply := IsSubring.mul_closed with subring36    obtain ⟨d, hd, clears⟩ := ih37    have localized : x ∈ localizationWithin(S, T, D) by simp [Subset]38    obtain ⟨inX, e, he, numerator⟩ := localizationWithin.membership.forward with localized39    have dIn : d ∈ S by simp [Subset]40    have eIn : e ∈ S by simp [Subset]41    have dInT : d ∈ T by simp [Subset]42    have eInT : e ∈ T by simp [Subset]43    have product := ClosedBinary.mem with denomClosed, hd, he44    refine ⟨S[d * e], product, ?_⟩45    intros u hu46    rw listSupport at hu47    have alternatives := insert.membership.forward with hu48    cases alternatives with equal | previous49    . rw equal50      have member := ClosedBinary.mem with multiply, dInT, numerator51      have equation : S[(d * e) * x] = S[d * (e * x)] by ring52      rwa equation53    . have tailBound := listSupport.subset with *54      have memberK : u ∈ K by simp [Subset]55      have memberLocal : u ∈ localizationWithin(S, T, D) by simp [Subset]56      have data := localizationWithin.membership.forward with memberLocal57      have inU := data.left58      have cleared := clears with u, previous59      have member := ClosedBinary.mem with multiply, eInT, cleared60      have equation : S[(d * e) * u] = S[e * (d * u)] by ring61      rwa equation6263theorem localizationWithin.clear_finite (K : Set)64  requires finite : Finite(K)65  requires included : K ⊆ localizationWithin(S, T, D)66  shows ∃ d ∈ D, ∀ x ∈ K, S[d * x] ∈ T67proof68  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite69  obtain ⟨d, hd, clears⟩ := localizationWithin.clear_list at B, plus, z, minus, times, unit, T, D, K, xs with *70  refine ⟨d, hd, ?_⟩71  intros x hx72  have covered : x ∈ listSupport{K}(xs) by simp [Subset]73  exact clears with x, covered7475end Rings7677section Algebras78variable (A add zero neg mul one B plus z minus times unit f T D M : Set)79notation ring R := (A, add, zero, neg, mul, one)80notation ring S := (B, plus, z, minus, times, unit)81hypothesis source : IsCommRing(R)82hypothesis target : IsCommRing(S)83hypothesis hom : IsRingHom(f, R, S)84hypothesis subalgebra : Subalgebra(f, R, S, T)85hypothesis denominators : Denominators(S, T, D)8687theorem localizationWithin.clear_finite_span88  requires finite : FiniteSpan(f, R, S, M)89  requires included : M ⊆ localizationWithin(S, T, D)90  shows ∃ d ∈ D, ∀ x ∈ M, S[d * x] ∈ T91proof92  have subring := Subalgebra.subring with source, target, hom, subalgebra93  have submodule := Subalgebra.submodule with source, target, hom, subalgebra94  have bound := IsSubring.subset_carrier with subring95  have denomBound := Denominators.subset with target, subring, denominators96  have ambient := Subset.transitive with denomBound, bound97  obtain ⟨G, finiteG, generators, spans⟩ := finite98  have localized := Subset.transitive with generators, included99  obtain ⟨d, hd, clears⟩ := localizationWithin.clear_finite with target, subring, denominators, finiteG, localized100  have dIn : d ∈ S by simp [Subset]101  have multipliers := rightMultipliers.submodule with source, target, hom, submodule, dIn102  have localBound := localizationWithin.subset at B, times, T, D103  have boundedG := Subset.transitive with localized, localBound104  have generatorsClear : G ⊆ rightMultipliers(B, times, T, d)105    intros u hu106    have inB : u ∈ S by simp [Subset]107    have cleared := clears with u, hu108    have commute : S[u * d] = S[d * u] by ring109    apply rightMultipliers.membership.backward110    rw commute111    refine ⟨inB, cleared⟩112  have allClear := linearSpan.least with source, target, hom, multipliers, generatorsClear113  rw spans at allClear114  refine ⟨d, hd, ?_⟩115  intros x hx116  have member : x ∈ rightMultipliers(B, times, T, d) by simp [Subset]117  obtain ⟨inB, cleared⟩ := rightMultipliers.membership.forward with member118  have commute : S[d * x] = S[x * d] by ring119  rwa commute120121end Algebras122