Localizations of commutative rings #
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 y
is a unit; - For all
z : S
, there exists(x, y) : R × M
such thatz * f y = f x
; - For all
x, y : R
such thatf x = f y
, there existsc ∈ M
such 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 (M : Submonoid R) (S : Type*)
is a typeclass expressing thatS
is a localization ofR
atM
, i.e. the canonical mapalgebraMap R S : R →+* S
is a localization map (satisfying the above properties).IsLocalization.mk' S
is a surjection sending(x, y) : R × M
tof x * (f y)⁻¹
IsLocalization.lift
is the ring homomorphism fromS
induced by a homomorphism fromR
which maps elements ofM
to invertible elements of the codomain.IsLocalization.map S Q
is the ring homomorphism fromS
toQ
which maps elements ofM
to elements ofT
IsLocalization.ringEquivOfRingEquiv
: ifR
andP
are isomorphic by an isomorphism sendingM
toT
, thenS
andQ
are isomorphic
Main results #
Localization M S
, a construction of the localization as a quotient type, defined inGroupTheory.MonoidLocalization
, hasCommRing
,Algebra R
andIsLocalization M
instances ifR
is a ring.Localization.Away
,Localization.AtPrime
andFractionRing
are abbreviations forLocalization
s and have their correspondingIsLocalization
instances
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 algebraMap
s.
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
The typeclass IsLocalization (M : Submonoid R) S
where S
is an R
-algebra
expresses that S
is isomorphic to the localization of R
at M
.
- map_units' : ∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)
Everything in the image of
algebraMap
is a unit - surj' : ∀ (z : S), ∃ (x : R × ↥M), z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
The
algebraMap
is surjective - exists_of_eq : ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ (c : ↥M), ↑c * x = ↑c * y
The kernel of
algebraMap
is contained in the annihilator ofM
; it is then equal to the annihilator bymap_units'
Instances
Everything in the image of algebraMap
is a unit
The algebraMap
is surjective
The kernel of algebraMap
is contained in the annihilator of M
;
it is then equal to the annihilator by map_units'
IsLocalization.toLocalizationWithZeroMap M S
shows S
is the monoid localization of
R
at M
.
Equations
- IsLocalization.toLocalizationWithZeroMap M S = { toFun := ⇑(algebraMap R S), map_one' := ⋯, map_mul' := ⋯, map_units' := ⋯, surj' := ⋯, exists_of_eq := ⋯, map_zero' := ⋯ }
Instances For
IsLocalization.toLocalizationMap M S
shows S
is the monoid localization of R
at M
.
Equations
- IsLocalization.toLocalizationMap M S = (IsLocalization.toLocalizationWithZeroMap M S).toLocalizationMap
Instances For
Given a localization map f : M →* N
, a section function sending z : N
to some
(x, y) : M × S
such that f x * (f y)⁻¹ = z
.
Equations
Instances For
Given z : S
, IsLocalization.sec M z
is defined to be a pair (x, y) : R × M
such
that z * f y = f x
(so this lemma is true by definition).
Given z : S
, IsLocalization.sec M z
is defined to be a pair (x, y) : R × M
such
that z * f y = f x
, so this lemma is just an application of S
's commutativity.
If M
contains 0
then the localization at M
is trivial.
IsLocalization.mk' S
is the surjection sending (x, y) : R × M
to
f x * (f y)⁻¹
.
Equations
- IsLocalization.mk' S x y = (IsLocalization.toLocalizationMap M S).mk' x y
Instances For
The localization of a Fintype
is a Fintype
. Cannot be an instance.
Equations
Instances For
Localizing at a submonoid with 0 inside it leads to the trivial ring.
Equations
Instances For
Equations
- IsLocalization.invertible_mk'_one s = { invOf := (algebraMap R S) ↑s, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
Given a localization map f : R →+* S
for a submonoid M ⊆ R
and a map of CommSemiring
s
g : R →+* P
such that g(M) ⊆ Units P
, f x = f y → g x = g y
for all x y : R
.
Given a localization map f : R →+* S
for a submonoid M ⊆ R
and a map of CommSemiring
s
g : R →+* P
such that g y
is invertible for all y : M
, the homomorphism induced from
S
to P
sending z : S
to g x * (g y)⁻¹
, where (x, y) : R × M
are such that
z = f x * (f y)⁻¹
.
Equations
- IsLocalization.lift hg = { toFun := (↑((IsLocalization.toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Given a localization map f : R →+* S
for a submonoid M ⊆ R
and a map of CommSemiring
s
g : R →* P
such that g y
is invertible for all y : M
, the homomorphism induced from
S
to P
maps f x * (f y)⁻¹
to g x * (g y)⁻¹
for all x : R, y ∈ M
.
See note [partially-applied ext lemmas]
See note [partially-applied ext lemmas]
To show j
and k
agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve 1
and *
.
Map a homomorphism g : R →+* P
to S →+* Q
, where S
and Q
are
localizations of R
and P
at M
and T
respectively,
such that g(M) ⊆ T
.
We send z : S
to algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹
, where
(x, y) : R × M
are such that z = f x * (f y)⁻¹
.
Equations
- IsLocalization.map Q g hy = IsLocalization.lift ⋯
Instances For
If CommSemiring
homs g : R →+* P, l : P →+* A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g
.
If CommSemiring
homs g : R →+* P, l : P →+* A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g
.
If S
, Q
are localizations of R
and P
at submonoids M, T
respectively, an
isomorphism j : R ≃+* P
such that j(M) = T
induces an isomorphism of localizations
S ≃+* Q
.
Equations
- IsLocalization.ringEquivOfRingEquiv S Q h H = { toFun := ⇑(IsLocalization.map Q ↑h ⋯), invFun := ⇑(IsLocalization.map S ↑h.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Injectivity of a map descends to the map induced on localizations.
Surjectivity of a map descends to the map induced on localizations.
Constructing a localization at a given submonoid #
Equations
- Localization.instUniqueLocalization = { toInhabited := OreLocalization.instInhabited, uniq := ⋯ }
For any given denominator b : M
, the map a ↦ a / b
is an AddMonoidHom
from R
to
Localization M
Equations
- Localization.mkAddMonoidHom b = { toFun := fun (a : R) => Localization.mk a b, map_zero' := ⋯, map_add' := ⋯ }
Instances For
A CommRing
S
which is the localization of a ring R
without zero divisors at a subset of
non-zero elements does not have zero divisors.
A CommRing
S
which is the localization of an integral domain R
at a subset of
non-zero elements is an integral domain.
The localization of an integral domain to a set of non-zero elements is an integral domain.