Localizations of commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

1. For all y ∈ M, f y is a unit;
2. For all z : S, there exists (x, y) : R × M such that z * f y = f x;
3. For all x, y : R, f x = f y iff there exists c ∈ M such that x * c = y * c.

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.:

variables (R S P Q : Type*) [comm_ring R] [comm_ring S] [comm_ring P] [comm_ring Q]
variables [algebra R S] [algebra P Q] (M : submonoid R) (T : submonoid P)

Main definitions #

• is_localization (M : submonoid R) (S : Type*) is a typeclass expressing that S is a localization of R at M, i.e. the canonical map algebra_map R S : R →+* S is a localization map (satisfying the above properties).
• is_localization.mk' S is a surjection sending (x, y) : R × M to f x * (f y)⁻¹
• is_localization.lift is the ring homomorphism from S induced by a homomorphism from R which maps elements of M to invertible elements of the codomain.
• is_localization.map S Q is the ring homomorphism from S to Q which maps elements of M to elements of T
• is_localization.ring_equiv_of_ring_equiv: if R and P are isomorphic by an isomorphism sending M to T, then S and Q are isomorphic
• is_localization.alg_equiv: if Q is another localization of R at M, then S and Q are isomorphic as R-algebras

Main results #

• localization M S, a construction of the localization as a quotient type, defined in group_theory.monoid_localization, has comm_ring, algebra R and is_localization M instances if R is a ring. localization.away, localization.at_prime and fraction_ring are abbreviations for localizations and have their corresponding is_localization 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 : localization_map 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 is_localization a predicate on the algebra_map R S, we can ensure the localization map commutes nicely with other algebra_maps.

To prove most lemmas about a localization map algebra_map R S in this file we invoke the corresponding proof for the underlying comm_monoid localization map is_localization.to_localization_map M S, which can be found in group_theory.monoid_localization and the namespace submonoid.localization_map.

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 algebra_map : 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 localization_map.mk' induced by any localization map.

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

Constructing a localization at a given submonoid #