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 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
- 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 comm_monoid localization_map underlying a comm_ring localization_map.
See group_theory.monoid_localization for its definition.
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.
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
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 := _, neg := has_neg.neg localization.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul (semigroup.to_has_mul (localization M)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, 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.
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.
Equations
- _ = _
The localization of R at the complement of a prime ideal is a local ring.
Equations
- _ = _
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
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
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
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 := _, neg := comm_ring.neg infer_instance, add_left_neg := _, add_comm := _, mul := comm_ring.mul infer_instance, mul_assoc := _, one := comm_ring.one infer_instance, one_mul := _, mul_one := _, 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
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 := _, neg := integral_domain.neg φ.to_integral_domain, 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 := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := φ.inv, 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 _
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
- of A = localization.of (non_zero_divisors A)
Equations
Given an integral domain A and a localization map to a field of fractions
f : A →+* K, we get an isomorphism between the field of fractions of A as a quotient
type and K.