Grace/Cumulus/Algebra/Field/Localization.g17

Open in Workbench Download source

Imports

ClearDenominators

Declarations

Source

1-- Localization in a field is the subring obtained by adjoining denominator inverses.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.Localization8import ClearDenominators910def denominatorInverses (B times unit D : Set) : Set :=11  {y ∈ B | ∃ d ∈ D, IsInverse(B, times, unit, d, y)}1213notation scoped denominatorInverses(R, D) => denominatorInverses(R.carrier, R.mul, R.one, D)1415theorem denominatorInverses.subset (B times unit D : Set)16  shows denominatorInverses(B, times, unit, D) ⊆ B17proof18  simp1920section Fields21variable (B plus z minus times unit T D : Set)22notation ring S := (B, plus, z, minus, times, unit)23hypothesis field : IsField(S)24hypothesis subring : IsSubring(S, T)25hypothesis denominators : Denominators(S, T, D)2627theorem denominatorInverses.exists (d : Set)28  requires member : d ∈ D29  shows ∃ y ∈ denominatorInverses(S, D), IsInverse(B, times, unit, d, y)30proof31  have ring := IsField.comm_ring with field32  have bound := IsSubring.subset_carrier with subring33  have denomBound := Denominators.subset with ring, subring, denominators34  have ambient := Subset.transitive with denomBound, bound35  have inB : d ∈ S by simp [Subset]36  have nonzero := Denominators.nonzero with ring, subring, denominators, member37  obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, inB, nonzero38  have yIn : y ∈ S by simp [IsInverse]39  have included : y ∈ denominatorInverses(S, D)40    exact denominatorInverses.membership.backward with ⟨yIn, d, member, inverse⟩41  refine ⟨y, included, inverse⟩4243theorem denominatorInverses.localized44  shows denominatorInverses(S, D) ⊆ localizationWithin(S, T, D)45proof46  have ring := IsField.comm_ring with field47  intros y hy48  obtain ⟨yIn, d, hd, inverse⟩ := denominatorInverses.membership.forward with hy49  exact localizationWithin.inverse_mem with ring, subring, denominators, hd, inverse5051theorem localizationWithin.generated52  shows localizationWithin(S, T, D) = generatedSubring(S, T ∪ denominatorInverses(S, D))53proof54  have ring := IsField.comm_ring with field55  have bound := IsSubring.subset_carrier with subring56  have inverseBound := denominatorInverses.subset at B, times, unit, D57  have generatorsBound : T ∪ denominatorInverses(S, D) ⊆ S58    settle with Subset, union2.membership59  have generated := generatedSubring.subring at B, plus, z, minus, times, unit, T ∪ denominatorInverses(S, D) with *60  have contains := generatedSubring.contains with ring, generatorsBound61  have includesT : T ⊆ generatedSubring(S, T ∪ denominatorInverses(S, D))62    settle with Subset, union2.membership63  have inverses : ∀ d ∈ D, ∃ y ∈ generatedSubring(S, T ∪ denominatorInverses(S, D)), IsInverse(B, times, unit, d, y)64    intros d hd65    obtain ⟨y, hy, inverse⟩ := denominatorInverses.exists with field, subring, denominators, hd66    have member : y ∈ generatedSubring(S, T ∪ denominatorInverses(S, D))67      settle with Subset, union2.membership68    refine ⟨y, member, inverse⟩69  have first := localizationWithin.least with ring, subring, denominators, generated, includesT, inverses70  have localized := localizationWithin.subring with ring, subring, denominators71  have original := localizationWithin.contains with ring, subring, denominators72  have inverseIncluded := denominatorInverses.localized with field, subring, denominators73  have generators : T ∪ denominatorInverses(S, D) ⊆ localizationWithin(S, T, D)74    settle with Subset, union2.membership75  have second := generatedSubring.least with ring, localized, generators76  exact Subset.antisymmetric with first, second7778theorem IsSubring.eq_field_of_uniform_denominator (d : Set)79  requires member : d ∈ D80  requires clears : ∀ x ∈ S, S[d * x] ∈ T81  shows T = S82proof83  have ring := IsField.comm_ring with field84  have ordinary := IsCommRing.ring with ring85  have bound := IsSubring.subset_carrier with subring86  have denomBound := Denominators.subset with ring, subring, denominators87  have ambient := Subset.transitive with denomBound, bound88  have dIn : d ∈ S by simp [Subset]89  have nonzero := Denominators.nonzero with ring, subring, denominators, member90  obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, dIn, nonzero91  have yIn := inverse.right.left92  have cancels := inverse.right.right.right93  apply Subset.antisymmetric94  . exact bound95    intros x hx96    have product := IsRing.mul_closed with ordinary, yIn, hx97    have numerator := clears with S[y * x], product98    have associate : S[d * (y * x)] = S[(d * y) * x] by ring99    rw [associate, cancels] at numerator100    have identity : S[1 * x] = x by ring101    rwa identity at numerator102103end Fields104105section Algebras106variable (A add zero neg mul one B plus z minus times unit f T D : Set)107notation ring R := (A, add, zero, neg, mul, one)108notation ring S := (B, plus, z, minus, times, unit)109hypothesis source : IsCommRing(R)110hypothesis field : IsField(S)111hypothesis hom : IsRingHom(f, R, S)112hypothesis subalgebra : Subalgebra(f, R, S, T)113hypothesis denominators : Denominators(S, T, D)114115theorem localizationWithin.eq_field_of_finite_module116  requires finite : FiniteAlgebraModule(f, R, S)117  requires fractions : localizationWithin(S, T, D) = S118  shows T = S119proof120  have target := IsField.comm_ring with field121  have subring := Subalgebra.subring with source, target, hom, subalgebra122  have finiteSpan := FiniteSpan.target_iff.backward with source, target, hom, finite123  have included : S ⊆ localizationWithin(S, T, D)124    rw fractions125    exact Subset.reflexive126  obtain ⟨d, hd, clears⟩ := localizationWithin.clear_finite_span with source, target, hom, subalgebra, denominators, finiteSpan, included127  exact IsSubring.eq_field_of_uniform_denominator with field, subring, denominators, hd, clears128129end Algebras130