Documentation

TauCeti.RingTheory.Localization.Away.FractionRing

The localization of a domain away from a nonzero element, inside a fraction field #

Let R be a domain with fraction field K (any commutative ring with IsFractionRing R K, as in Mathlib's IsFractionRing API) and let f be a nonzero element of R. The localization Localization.Away f embeds in K, and K is again its fraction field. This is the analogue for Localization.Away of TauCeti/RingTheory/Localization/AtPrime.lean, built the same way from IsLocalization.localizationAlgebraOfSubmonoidLe, here for the inequality powers_le_nonZeroDivisors_of_noZeroDivisors.

Unlike the prime case, the construction needs the hypothesis f ≠ 0 (for f = 0 the localization is the zero ring, which has no map to the nonzero ring K), so the declarations below are a def and theorems about it rather than global instances. A consumer installs them locally.

Main declarations #

source
@[reducible, inline]
noncomputable abbrev Localization.Away.algebraOfIsFractionRing {R : Type u_1} [CommRing R] [IsDomain R] (K : Type u_2) [CommRing K] [Algebra R K] [IsFractionRing R K] {f : R} (hf : f ≠ 0) :
Algebra (Away f) K

For a nonzero f in a domain R, the localization R_f maps to any fraction field K of R: the Algebra structure lifting algebraMap R K, which inverts the powers of f because they are nonzero.

Instances For
    source
    theorem Localization.Away.isScalarTower_of_isFractionRing {R : Type u_1} [CommRing R] [IsDomain R] (K : Type u_2) [CommRing K] [Algebra R K] [IsFractionRing R K] {f : R} (hf : f ≠ 0) :
    IsScalarTower R (Away f) K

    The map algebraOfIsFractionRing from R_f to a fraction field K of R extends algebraMap R K.

    source
    theorem Localization.Away.isFractionRing {R : Type u_1} [CommRing R] [IsDomain R] (K : Type u_2) [CommRing K] [Algebra R K] [IsFractionRing R K] {f : R} (hf : f ≠ 0) :
    IsFractionRing (Away f) K

    Along algebraOfIsFractionRing, a fraction field K of a domain R is a fraction field of the localization R_f away from a nonzero f.