Localizations of commutative rings #
This file contains various basic results on localizations.
We characterize the localization of a commutative ring R at a submonoid M up to
isomorphism; that is, a commutative ring S is the localization of R at M iff we can find a
ring homomorphism f : R →+* S satisfying 3 properties:
- For all
y ∈ M,f yis a unit; - For all
z : S, there exists(x, y) : R × Msuch thatz * f y = f x; - For all
x, y : Rsuch thatf x = f y, there existsc ∈ Msuch thatx * c = y * c. (The converse is a consequence of 1.)
In the following, let R, P be commutative rings, S, Q be R- and P-algebras
and M, T be submonoids of R and P respectively, e.g.:
variable (R S P Q : Type*) [CommRing R] [CommRing S] [CommRing P] [CommRing Q]
variable [Algebra R S] [Algebra P Q] (M : Submonoid R) (T : Submonoid P)
Main definitions #
IsLocalization.algEquiv: ifQis another localization ofRatM, thenSandQare isomorphic asR-algebras
Implementation notes #
In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite one
structure with an isomorphic one; one way around this is to isolate a predicate characterizing
a structure up to isomorphism, and reason about things that satisfy the predicate.
A previous version of this file used a fully bundled type of ring localization maps,
then used a type synonym f.codomain for f : LocalizationMap M S to instantiate the
R-algebra structure on S. This results in defining ad-hoc copies for everything already
defined on S. By making IsLocalization a predicate on the algebraMap R S,
we can ensure the localization map commutes nicely with other algebraMaps.
To prove most lemmas about a localization map algebraMap R S in this file we invoke the
corresponding proof for the underlying CommMonoid localization map
IsLocalization.toLocalizationMap M S, which can be found in GroupTheory.MonoidLocalization
and the namespace Submonoid.LocalizationMap.
To reason about the localization as a quotient type, use mk_eq_of_mk' and associated lemmas.
These show the quotient map mk : R → M → Localization M equals the surjection
LocalizationMap.mk' induced by the map algebraMap : R →+* Localization M.
The lemma mk_eq_of_mk' hence gives you access to the results in the rest of the file,
which are about the LocalizationMap.mk' induced by any localization map.
The proof that "a CommRing K which is the localization of an integral domain R at R \ {0}
is a field" is a def rather than an instance, so if you want to reason about a field of
fractions K, assume [Field K] instead of just [CommRing K].
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
If S, Q are localizations of R at the submonoid M respectively,
there is an isomorphism of localizations S ≃ₐ[R] Q.
Equations
- IsLocalization.algEquiv M S Q = { toEquiv := (IsLocalization.ringEquivOfRingEquiv S Q (RingEquiv.refl R) ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
The localization at a module of units is isomorphic to the ring.
Equations
- IsLocalization.atUnits R M H = AlgEquiv.ofBijective (Algebra.ofId R S) ⋯
Instances For
If S₁ is the localization of R at M₁ and S₂ is the localization of
R at M₂, then every localization T of S₂ at M₁ is also a localization of
S₁ at M₂, in other words M₁⁻¹M₂⁻¹R can be identified with M₂⁻¹M₁⁻¹R.
Alias of Localization.mk_natCast.
The localization of R at M as a quotient type is isomorphic to any other localization.
Equations
- Localization.algEquiv M S = IsLocalization.algEquiv M (Localization M) S
Instances For
The localization of a singleton is a singleton. Cannot be an instance due to metavariables.
Equations
- IsLocalization.unique R Rₘ M = ⋯.unique
Instances For
Alias of Localization.mk_intCast.
If R is a field, then localizing at a submonoid not containing 0 adds no new elements.
If R is a field, then localizing at a submonoid not containing 0 adds no new elements.
Definition of the natural algebra induced by the localization of an algebra.
Given an algebra R → S, a submonoid R of M, and a localization Rₘ for M,
let Sₘ be the localization of S to the image of M under algebraMap R S.
Then this is the natural algebra structure on Rₘ → Sₘ, such that the entire square commutes,
where localization_map.map_comp gives the commutativity of the underlying maps.
This instance can be helpful if you define Sₘ := Localization (Algebra.algebraMapSubmonoid S M),
however we will instead use the hypotheses [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] in lemmas
since the algebra structure may arise in different ways.
Equations
- localizationAlgebra M S = (IsLocalization.map Sₘ (algebraMap R S) ⋯).toAlgebra
Instances For
If the square below commutes, the bottom map is uniquely specified:
R → S
↓ ↓
Rₘ → Sₘ
If the square below commutes, the bottom map is uniquely specified:
R → S
↓ ↓
Rₘ → Sₘ
Injectivity of the underlying algebraMap descends to the algebra induced by localization.