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
,f x = f y
iff there existsc ∈ M
such thatx * c = y * c
.
Given such a localization map f : R →+* S
, we can define the surjection
localization_map.mk'
sending (x, y) : R × M
to f x * (f y)⁻¹
, and
localization_map.lift
, the homomorphism from S
induced by a homomorphism from R
which maps
elements of M
to invertible elements of the codomain. Similarly, given commutative rings
P, Q
, a submonoid T
of P
and a localization map for T
from P
to Q
, then a homomorphism
g : R →+* P
such that g(M) ⊆ T
induces a homomorphism of localizations,
localization_map.map
, from S
to Q
.
We treat the special case of localizing away from an element in the sections away_map
and away
.
We show the localization as a quotient type, defined in group_theory.monoid_localization
as
submonoid.localization
, is a comm_ring
and that the natural ring hom
of : R →+* localization M
is a localization map.
We show that a localization at the complement of a prime ideal is a local ring.
We prove some lemmas about the R
-algebra structure of S
.
When R
is an integral domain, we define fraction_map R K
as an abbreviation for
localization (non_zero_divisors R) K
, the natural map to R
's field of fractions.
We show that a comm_ring
K
which is the localization of an integral domain R
at R \ {0}
is a field. We use this to show the field of fractions as a quotient type, fraction_ring
, is
a field.
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 ring localization map is defined to be a localization map of the underlying comm_monoid
(a
submonoid.localization_map
) which is also a ring hom. To prove most lemmas about a
localization_map
f
in this file we invoke the corresponding proof for the underlying
comm_monoid
localization map f.to_localization_map
, which can be found in
group_theory.monoid_localization
and the namespace submonoid.localization_map
.
To apply a localization map f
as a function, we use f.to_map
, as coercions don't work well for
this structure.
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
localization_map.mk'
induced by the map of : localization_map M (localization M)
(where of
establishes the localization as a quotient type satisfies the characteristic
predicate). The lemma mk_eq_of_mk'
hence gives you access to the results in the rest of the file,
which are about the localization_map.mk'
induced by any localization map.
We define a copy of the localization map f
's codomain S
carrying the data of f
so that
instances on S
induced by f
can 'know' the map needed to induce the instance.
The proof that "a comm_ring
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 [comm_ring K]
.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
The comm_monoid
localization_map
underlying a comm_ring
localization_map
.
See group_theory.monoid_localization
for its definition.
- to_fun : R → S
- map_one' : c.to_fun 1 = 1
- map_mul' : ∀ (x y : R), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : R), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_units' : ∀ (y : ↥M), is_unit (c.to_fun ↑y)
- surj' : ∀ (z : S), ∃ (x : R × ↥M), z * c.to_fun ↑(x.snd) = c.to_fun x.fst
- eq_iff_exists' : ∀ (x y : R), c.to_fun x = c.to_fun y ↔ ∃ (c : ↥M), x * ↑c = y * ↑c
The type of ring homomorphisms satisfying the characteristic predicate: if f : R →+* S
satisfies this predicate, then S
is isomorphic to the localization of R
at M
.
We later define an instance coercing a localization map f
to its codomain S
so
that instances on S
induced by f
can 'know' the map needed to induce the instance.
The ring hom underlying a localization_map
.
Makes a localization map from a comm_ring
hom satisfying the characteristic predicate.
Equations
- f.to_localization_map H1 H2 H3 = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, map_units' := H1, surj' := H2, eq_iff_exists' := H3}
Makes a comm_ring
localization map from an additive comm_monoid
localization map of
comm_ring
s.
Equations
- f.to_ring_localization h = {to_fun := (ring_hom.mk' f.to_monoid_hom h).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, map_units' := _, surj' := _, eq_iff_exists' := _}
We define a copy of the localization map f
's codomain S
carrying the data of f
so that
instances on S
induced by f
can 'know` the map needed to induce the instance.
Equations
- localization_map.codomain.comm_ring f = _inst_2
Equations
- localization_map.codomain.field f = _inst_4
Short for to_ring_hom
; used for applying a localization map as a function.
Given a : S
, S
a localization of R
, is_integer a
iff a
is in the image of
the localization map from R
to S
.
Each element a : S
has an M
-multiple which is an integer.
This version multiplies a
on the right, matching the argument order in localization_map.surj
.
Each element a : S
has an M
-multiple which is an integer.
This version multiplies a
on the left, matching the argument order in the has_scalar
instance.
Given z : S
, f.to_localization_map.sec 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
, f.to_localization_map.sec 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.
We can clear the denominators of a finite set of fractions.
Given a localization map f : R →+* S
, the surjection sending (x, y) : R × M
to
f x * (f y)⁻¹
.
Equations
- f.mk' x y = f.to_localization_map.mk' x y
Given a localization map f : R →+* S
for a submonoid M ⊆ R
and a map of comm_ring
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 comm_ring
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
- f.lift hg = ring_hom.mk' (f.to_localization_map.lift hg) _
Given a localization map f : R →+* S
for a submonoid M ⊆ R
and a map of comm_ring
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
.
Given two localization maps f : R →+* S, k : R →+* P
for a submonoid M ⊆ R
,
the hom from P
to S
induced by f
is left inverse to the hom from S
to P
induced by k
.
Given a comm_ring
homomorphism g : R →+* P
where for submonoids M ⊆ R, T ⊆ P
we have
g(M) ⊆ T
, the induced ring homomorphism from the localization of R
at M
to the
localization of P
at T
: if f : R →+* S
and k : P →+* Q
are localization maps for M
and T
respectively, we send z : S
to k (g x) * (k (g y))⁻¹
, where (x, y) : R × M
are
such that z = f x * (f y)⁻¹
.
If comm_ring
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 comm_ring
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
.
Given localization maps f : R →+* S, k : P →+* Q
for submonoids M, T
respectively, an
isomorphism j : R ≃+* P
such that j(M) = T
induces an isomorphism of localizations
S ≃+* Q
.
Equations
Given x : R
, the type of homomorphisms f : R →* S
such that S
is isomorphic to the localization of R
at the submonoid generated by x
.
Equations
- localization_map.away_map x S' = localization_map (submonoid.powers x) S'
Given x : R
and a localization map F : R →+* S
away from x
, inv_self
is (F x)⁻¹
.
Equations
- localization_map.away_map.inv_self x F = localization_map.mk' F 1 ⟨x, _⟩
Given x : R
, a localization map F : R →+* S
away from x
, and a map of comm_ring
s
g : R →+* P
such that g x
is invertible, the homomorphism induced from S
to P
sending
z : S
to g y * (g x)⁻ⁿ
, where y : R, n : ℕ
are such that z = F y * (F x)⁻ⁿ
.
Equations
- localization_map.away_map.lift x F hg = localization_map.lift F _
Given x y : R
and localization maps F : R →+* S, G : R →+* P
away from x
and x * y
respectively, the homomorphism induced from S
to P
.
Equations
- localization_map.away_to_away_right x F y G = ↑(localization_map.away_map.lift x F _)
Equations
- localization.has_neg = {neg := λ (z : localization M), con.lift_on z (λ (x : R × ↥M), localization.mk (-x.fst) x.snd) localization.has_neg._proof_1}
Equations
- localization.has_zero = {zero := localization.mk 0 1}
Equations
- localization.comm_ring = {add := has_add.add localization.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := ring.nsmul._default 0 has_add.add localization.comm_ring._proof_4 localization.comm_ring._proof_5, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg localization.has_neg, sub := λ (x y : localization M), x + -y, sub_eq_add_neg := _, gsmul := ring.gsmul._default has_add.add localization.comm_ring._proof_9 0 localization.comm_ring._proof_10 localization.comm_ring._proof_11 (ring.nsmul._default 0 has_add.add localization.comm_ring._proof_4 localization.comm_ring._proof_5) localization.comm_ring._proof_12 localization.comm_ring._proof_13 has_neg.neg, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (mul_one_class.to_has_mul (localization M)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := comm_monoid.npow (localization.comm_monoid M), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Natural hom sending x : R
, R
a comm_ring
, to the equivalence class of
(x, 1)
in the localization of R
at a submonoid.
Equations
Given a localization map f : R →+* S
for a submonoid M
, we get an isomorphism
between the localization of R
at M
as a quotient type and S
.
Given x : R
, the natural hom sending y : R
, R
a comm_ring
, to the equivalence class
of (y, 1)
in the localization of R
at the submonoid generated by x
.
Equations
Given x : R
and a localization map f : R →+* S
away from x
, we get an isomorphism between
the localization of R
at the submonoid generated by x
as a quotient type and S
.
A localization map from R
to S
where the submonoid is the complement of a prime
ideal of R
.
Equations
The localization of R
at the complement of a prime ideal, as a quotient type.
Equations
When f
is a localization map from R
at the complement of a prime ideal I
, we use a
copy of the localization map f
's codomain S
carrying the data of f
so that the local_ring
instance on S
can 'know' the map needed to induce the instance.
The localization of R
at the complement of a prime ideal is a local ring.
If S
is the localization of R
at a submonoid, the ordering of ideals of S
is
embedded in the ordering of ideals of R
.
Equations
- f.order_embedding = {to_embedding := {to_fun := λ (J : ideal S), ideal.comap f.to_map J, inj' := _}, map_rel_iff' := _}
If R
is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R
that are disjoint from M
.
This lemma gives the particular case for an ideal and its comap,
see le_rel_iso_of_prime
for the more general relation isomorphism
If R
is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R
that are disjoint from M
.
This lemma gives the particular case for an ideal and its map,
see le_rel_iso_of_prime
for the more general relation isomorphism, and the reverse implication
If R
is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R
that are disjoint from M
quotient_map
applied to maximal ideals of a localization is surjective
.
The quotient by a maximal ideal is a field, so inverses to elements already exist,
and the localization necessarily maps the equivalence class of the inverse in the localization
algebra
section #
Defines the R
-algebra instance on a copy of S
carrying the data of the localization map
f
needed to induce the R
-algebra structure.
We use a copy of the localization map f
's codomain S
carrying the data of f
so that the
R
-algebra instance on S
can 'know' the map needed to induce the R
-algebra structure.
Equations
- f.algebra = f.to_map.to_algebra
Equations
Map from ideals of R
to submodules of S
induced by f
.
Equations
- f.coe_submodule I = submodule.map f.lin_coe I
Given a localization map f : R →+* S
for a submonoid M
, we get an R
-preserving
isomorphism between the localization of R
at M
as a quotient type and S
.
Equations
- localization.alg_equiv_of_quotient f = {to_fun := (localization.ring_equiv_of_quotient f).to_fun, inv_fun := (localization.ring_equiv_of_quotient f).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
coeff_integer_normalization p
gives the coefficients of the polynomial
integer_normalization p
Equations
- localization_map.coeff_integer_normalization p i = dite (i ∈ p.support) (λ (hi : i ∈ p.support), classical.some _) (λ (hi : i ∉ p.support), 0)
integer_normalization g
normalizes g
to have integer coefficients
by clearing the denominators
Equations
- f.integer_normalization p = ∑ (i : ℕ) in p.support, ⇑(polynomial.monomial i) (localization_map.coeff_integer_normalization p i)
A comm_ring
S
which is the localization of an integral domain R
at a subset of
non-zero elements is an integral domain.
Equations
- f.integral_domain_of_le_non_zero_divisors hM = {add := comm_ring.add infer_instance, add_assoc := _, zero := comm_ring.zero infer_instance, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg infer_instance, sub := comm_ring.sub infer_instance, sub_eq_add_neg := _, gsmul := comm_ring.gsmul infer_instance, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul infer_instance, mul_assoc := _, one := comm_ring.one infer_instance, one_mul := _, mul_one := _, npow := comm_ring.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
The localization at of an integral domain to a set of non-zero elements is an integral domain
The localization of an integral domain at the complement of a prime ideal is an integral domain.
The unique maximal ideal of the localization at I.prime_compl
lies over the ideal I
.
The image of I
in the localization at I.prime_compl
is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure at_prime.local_ring
If R
is a field, then localizing at a submonoid not containing 0
adds no new elements.
Localization map from an integral domain R
to its field of fractions.
Equations
- fraction_map R K = localization_map (non_zero_divisors R) K
A comm_ring
K
which is the localization of an integral domain R
at R - {0}
is an
integral domain.
Equations
- φ.to_integral_domain = localization_map.integral_domain_of_le_non_zero_divisors φ fraction_map.to_integral_domain._proof_1
The inverse of an element in the field of fractions of an integral domain.
A comm_ring
K
which is the localization of an integral domain R
at R - {0}
is a
field.
Equations
- φ.to_field = {add := integral_domain.add φ.to_integral_domain, add_assoc := _, zero := integral_domain.zero φ.to_integral_domain, zero_add := _, add_zero := _, nsmul := integral_domain.nsmul φ.to_integral_domain, nsmul_zero' := _, nsmul_succ' := _, neg := integral_domain.neg φ.to_integral_domain, sub := integral_domain.sub φ.to_integral_domain, sub_eq_add_neg := _, gsmul := integral_domain.gsmul φ.to_integral_domain, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := integral_domain.mul φ.to_integral_domain, mul_assoc := _, one := integral_domain.one φ.to_integral_domain, one_mul := _, mul_one := _, npow := integral_domain.npow φ.to_integral_domain, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := φ.inv, div := div_inv_monoid.div._default integral_domain.mul _ integral_domain.one _ _ integral_domain.npow _ _ φ.inv, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default integral_domain.mul _ integral_domain.one _ _ integral_domain.npow _ _ φ.inv, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
Given an integral domain A
, a localization map to its fields of fractions
f : A →+* K
, and an injective ring hom g : A →+* L
where L
is a field, we get a
field hom sending z : K
to g x * (g y)⁻¹
, where (x, y) : A × (non_zero_divisors A)
are
such that z = f x * (f y)⁻¹
.
Equations
- f.lift hg = localization_map.lift f _
Given an integral domain A
, a localization map to its fields of fractions
f : A →+* K
, and an injective ring hom g : A →+* L
where L
is a field,
field hom induced from K
to L
maps f x / f y
to g x / g y
for all
x : A, y ∈ non_zero_divisors A
.
Given integral domains A, B
and localization maps to their fields of fractions
f : A →+* K, g : B →+* L
and an injective ring hom j : A →+* B
, we get a field hom
sending z : K
to g (j x) * (g (j y))⁻¹
, where (x, y) : A × (non_zero_divisors A)
are
such that z = f x * (f y)⁻¹
.
Equations
- f.map g hj = localization_map.map f _ g
Given integral domains A, B
and localization maps to their fields of fractions
f : A →+* K, g : B →+* L
, an isomorphism j : A ≃+* B
induces an isomorphism of
fields of fractions K ≃+* L
.
Equations
The cast from int
to rat
as a fraction_map
.
Equations
- fraction_map.int.fraction_map = {to_fun := coe coe_to_lift, map_one' := fraction_map.int.fraction_map._proof_1, map_mul' := fraction_map.int.fraction_map._proof_2, map_zero' := fraction_map.int.fraction_map._proof_3, map_add' := fraction_map.int.fraction_map._proof_4, map_units' := fraction_map.int.fraction_map._proof_5, surj' := fraction_map.int.fraction_map._proof_6, eq_iff_exists' := fraction_map.int.fraction_map._proof_7}
A field is algebraic over the ring A
iff it is algebraic over the field of fractions of A
.
f.num x
is the numerator of x : f.codomain
as a reduced fraction.
Equations
- φ.num x = classical.some _
f.num x
is the denominator of x : f.codomain
as a reduced fraction.
Equations
- φ.denom x = classical.some _
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 algebra_map 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
Equations
- localization_algebra M f g = (f.map _ g).to_algebra
Injectivity of a map descends to the map induced on localizations.
Injectivity of the underlying algebra_map
descends to the algebra induced by localization.
Given a particular witness to an element being algebraic over an algebra R → S
,
We can localize to a submonoid containing the leading coefficient to make it integral.
Explicitly, the map between the localizations will be an integral ring morphism
If R → S
is an integral extension, M
is a submonoid of R
,
Rₘ
is the localization of R
at M
,
and Sₘ
is the localization of S
at the image of M
under the extension map,
then the induced map Rₘ → Sₘ
is also an integral extension
If the field L
is an algebraic extension of the integral domain A
,
the integral closure of A
in L
has fraction field L
.
Equations
- integral_closure.fraction_map_of_algebraic alg inj = (algebra_map ↥(integral_closure A L) L).to_localization_map integral_closure.fraction_map_of_algebraic._proof_1 _ integral_closure.fraction_map_of_algebraic._proof_3
If the field L
is a finite extension of the fraction field of the integral domain A
,
the integral closure of A
in L
has fraction field L
.
The fraction field of an integral domain as a quotient type.
Equations
Natural hom sending x : A
, A
an integral domain, to the equivalence class of
(x, 1)
in the field of fractions of A
.
Equations
Equations
Given an integral domain A
and a localization map to a field of fractions
f : A →+* K
, we get an A
-isomorphism between the field of fractions of A
as a quotient
type and K
.