Grace/Cumulus/Algebra/Field/LocalizationObstruction.g17

Open in Workbench Download source

Imports

Localization · Powers · Set.OrderTransport

Declarations

Source

1-- A homomorphism separating denominators from a nonzero kernel element obstructs localization.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.LocalizationObstruction8import Localization9import Powers10import Set.OrderTransport1112section Maps13variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring S := (B, plus, z, minus, times, unit)16notation ring U := (C, sum, o, inverse, product, e)17hypothesis source : IsCommRing(R)18hypothesis target : IsCommRing(S)19hypothesis residue : IsCommRing(U)20hypothesis embedding : IsRingHom(g, R, S)21hypothesis injective : InjectiveBetween(g, R, S)22hypothesis evaluation : IsRingHom(h, R, U)23hypothesis bounded : D ⊆ R24hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]2526theorem localizationWithin.excludes_kernel_inverse (p y : Set)27  requires member : p ∈ R28  requires vanishes : h(p) = U[0]29  requires inverseP : IsInverse(B, times, unit, g(p), y)30  shows ¬(y ∈ localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)))31proof32  have ordinary := IsCommRing.ring with source33  have imageP := IsRingHom.closed with embedding, member34  have data := inverseP35  have inY := data.right.left36  have cancels := data.right.right.left37  intro localized38  obtain ⟨inB, d, hd, numerator⟩ := localizationWithin.membership.forward with localized39  obtain ⟨inD, a, ha, valueD⟩ := functionImage.membership.forward with hd40  obtain ⟨inProduct, q, hq, valueQ⟩ := functionImage.membership.forward with numerator41  have aIn : a ∈ R by simp [Subset]42  have qpIn := IsRing.mul_closed with ordinary, hq, member43  have mapped := IsRingHom.mul with embedding, hq, member44  have equation : g(R[q * p]) = g(a)45    have rearrange : S[(d * y) * g(p)] = S[d * (y * g(p))] by ring46    rw cancels at rearrange47    have identity : S[d * 1] = d by ring48    cc49  have equal := Injective.apply_cancel with injective, qpIn, aIn, equation50  have evaluated := IsRingHom.mul with evaluation, hq, member51  have valueQin := IsRingHom.closed with evaluation, hq52  have zeroProduct : U[h(q) * 0] = U[0] by ring53  have zeroValue : h(a) = U[0] by cc54  have distinct := avoids with a, ha55  exact distinct with zeroValue5657end Maps5859section Nonfields60variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D T : Set)61notation ring R := (A, add, zero, neg, mul, one)62notation ring S := (B, plus, z, minus, times, unit)63notation ring U := (C, sum, o, inverse, product, e)64notation ring L := S ↾ T65hypothesis source : IsCommRing(R)66hypothesis target : IsCommRing(S)67hypothesis residue : IsCommRing(U)68hypothesis embedding : IsRingHom(g, R, S)69hypothesis injective : InjectiveBetween(g, R, S)70hypothesis evaluation : IsRingHom(h, R, U)71hypothesis bounded : D ⊆ R72hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]73hypothesis denominatorOne : R[1] ∈ D74hypothesis carrier : T = localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S))7576theorem localizationWithin.not_field_of_kernel (p : Set)77  requires member : p ∈ R78  requires nonzero : p ≠ R[0]79  requires vanishes : h(p) = U[0]80  shows ¬IsField(L)81proof82  have ordinary := IsCommRing.ring with source83  have zeroIn := IsRing.zero_in_carrier with ordinary84  have zeroValue := IsRingHom.zero with embedding85  have oneValue := IsRingHom.one with embedding86  have image := IsRingHom.closed with embedding, member87  have targetRing := IsCommRing.ring with target88  have monoid := IsRing.multiplicative with targetRing89  have oneIn := IsMonoid.unit_in_carrier with monoid90  have multiplication : IsMagma(B, times) by simp [IsMonoid, IsSemigroup]91  have subset : T ⊆ S92    rw carrier93    exact localizationWithin.subset94  have imageNonzero : g(p) ≠ S[0]95    intro equal96    have mapped : g(p) = g(R[0]) by cc97    have impossible := Injective.apply_cancel with injective, member, zeroIn, mapped98    exact nonzero with impossible99  have function := IsRingHom.function with embedding100  have numerator := functionImage.value with function, member101  have denominator : S[1] ∈ functionImage(g, D, B)102    apply functionImage.membership.backward103    refine ⟨oneIn, R[1], denominatorOne, ?_⟩104    cc105  have localized : g(p) ∈ T106    rw carrier107    apply localizationWithin.membership.backward108    refine ⟨image, S[1], denominator, ?_⟩109    have identity : S[1 * g(p)] = g(p) by ring110    rwa identity111  intro field112  obtain ⟨y, inverseP⟩ := IsField.inverse_exists with field, localized, imageNonzero113  unfold IsInverse at inverseP114  have inY := inverseP.right.left115  have ambientY : y ∈ S by simp [Subset]116  have leftValue := restrictBinary.value_on_subset at B, T, times, y, g(p) with *117  have rightValue := restrictBinary.value_on_subset at B, T, times, g(p), y with *118  have leftInverse : S[y * g(p)] = S[1] by cc119  have rightInverse : S[g(p) * y] = S[1] by cc120  have ambientInverse : IsInverse(B, times, unit, g(p), y) by simp [IsInverse]121  have excluded := localizationWithin.excludes_kernel_inverse with source, target, residue, embedding, injective, evaluation, bounded, avoids, member, vanishes, ambientInverse122  rw carrier at inY123  exact excluded with inY124125end Nonfields126127section Fields128variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D : Set)129notation ring R := (A, add, zero, neg, mul, one)130notation ring S := (B, plus, z, minus, times, unit)131notation ring U := (C, sum, o, inverse, product, e)132hypothesis source : IsCommRing(R)133hypothesis field : IsField(S)134hypothesis residue : IsCommRing(U)135hypothesis embedding : IsRingHom(g, R, S)136hypothesis injective : InjectiveBetween(g, R, S)137hypothesis evaluation : IsRingHom(h, R, U)138hypothesis bounded : D ⊆ R139hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]140141theorem localizationWithin.proper_of_kernel (p : Set)142  requires member : p ∈ R143  requires nonzero : p ≠ R[0]144  requires vanishes : h(p) = U[0]145  shows localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)) ≠ S146proof147  have target := IsField.comm_ring with field148  have ordinary := IsCommRing.ring with source149  have zeroIn := IsRing.zero_in_carrier with ordinary150  have zeroValue := IsRingHom.zero with embedding151  have image := IsRingHom.closed with embedding, member152  have imageNonzero : g(p) ≠ S[0]153    intro zero154    have equal : g(p) = g(R[0]) by cc155    have impossible := Injective.apply_cancel with injective, member, zeroIn, equal156    exact nonzero with impossible157  obtain ⟨y, inverseP⟩ := IsField.inverse_exists with field, imageNonzero158  have excluded := localizationWithin.excludes_kernel_inverse with source, target, residue, embedding, injective, evaluation, bounded, avoids, member, vanishes, inverseP159  have inY : y ∈ S by simp [IsInverse]160  intro equal161  have included : y ∈ localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)) by rwa equal162  exact excluded with included163164end Fields165