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 yis a unit; - For all
z : S, there exists(x, y) : R × Msuch thatz * f y = f x; - For all
x, y : R,f x = f yiff there existsc ∈ Msuch 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_rings.
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_rings
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_rings
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_rings
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_rings
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.