Documentation

Mathlib.RingTheory.Localization.Defs

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:

  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 such that f x = f y, there exists c ∈ M such that x * 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 #

Main results #

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

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

class IsLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] :

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.

Instances
theorem isLocalization_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] :
IsLocalization M S (∀ (y : M), IsUnit ((algebraMap R S) y)) (∀ (z : S), ∃ (x : R × M), z * (algebraMap R S) x.2 = (algebraMap R S) x.1) ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y∃ (c : M), c * x = c * y
theorem IsLocalization.map_units {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (y : M) :
IsUnit ((algebraMap R S) y)

Everything in the image of algebraMap is a unit

theorem IsLocalization.surj {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
∃ (x : R × M), z * (algebraMap R S) x.2 = (algebraMap R S) x.1

The algebraMap is surjective

theorem IsLocalization.eq_iff_exists {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {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 of M; it is then equal to the annihilator by map_units'

theorem IsLocalization.injective_iff_isRegular {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] :
Function.Injective (algebraMap R S) ∀ (c : M), IsRegular c
theorem IsLocalization.of_le {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (N : Submonoid R) (h₁ : M N) (h₂ : rN, IsUnit ((algebraMap R S) r)) :
theorem IsLocalization.of_le_of_exists_dvd {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (N : Submonoid R) (h₁ : M N) (h₂ : nN, mM, n m) :
theorem IsLocalization.algebraMap_isUnit_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} :
IsUnit ((algebraMap R S) x) mM, x m

IsLocalization.toLocalizationWithZeroMap M S shows S is the monoid localization of R at M.

Equations
@[reducible, inline]

IsLocalization.toLocalizationMap M S shows S is the monoid localization of R at M.

Equations
@[simp]
theorem IsLocalization.surj₂ {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (z w : S) :
∃ (z' : R) (w' : R) (d : M), z * (algebraMap R S) d = (algebraMap R S) z' w * (algebraMap R S) d = (algebraMap R S) w'
noncomputable def IsLocalization.sec {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
R × M

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
theorem IsLocalization.sec_spec {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
z * (algebraMap R S) (sec M z).2 = (algebraMap R S) (sec M z).1

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

theorem IsLocalization.sec_spec' {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
(algebraMap R S) (sec M z).1 = (algebraMap R S) (sec M z).2 * z

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.

theorem IsLocalization.subsingleton {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (h : 0 M) :

If M contains 0 then the localization at M is trivial.

theorem IsLocalization.map_right_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x y : R} {c : M} (h : (algebraMap R S) (c * x) = (algebraMap R S) (c * y)) :
(algebraMap R S) x = (algebraMap R S) y
theorem IsLocalization.map_left_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x y : R} {c : M} (h : (algebraMap R S) (x * c) = (algebraMap R S) (y * c)) :
(algebraMap R S) x = (algebraMap R S) y
theorem IsLocalization.eq_zero_of_fst_eq_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {z : S} {x : R} {y : M} (h : z * (algebraMap R S) y = (algebraMap R S) x) (hx : x = 0) :
z = 0
theorem IsLocalization.map_eq_zero_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (r : R) :
(algebraMap R S) r = 0 ∃ (m : M), m * r = 0
noncomputable def IsLocalization.mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
S

IsLocalization.mk' S is the surjection sending (x, y) : R × M to f x * (f y)⁻¹.

Equations
Instances For
@[simp]
theorem IsLocalization.mk'_sec {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
mk' S (sec M z).1 (sec M z).2 = z
theorem IsLocalization.mk'_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : M) :
mk' S (x₁ * x₂) (y₁ * y₂) = mk' S x₁ y₁ * mk' S x₂ y₂
theorem IsLocalization.mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) :
mk' S x 1 = (algebraMap R S) x
@[simp]
theorem IsLocalization.mk'_spec {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
mk' S x y * (algebraMap R S) y = (algebraMap R S) x
@[simp]
theorem IsLocalization.mk'_spec' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
(algebraMap R S) y * mk' S x y = (algebraMap R S) x
@[simp]
theorem IsLocalization.mk'_spec_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (hy : y M) :
mk' S x y, hy * (algebraMap R S) y = (algebraMap R S) x
@[simp]
theorem IsLocalization.mk'_spec'_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (hy : y M) :
(algebraMap R S) y * mk' S x y, hy = (algebraMap R S) x
theorem IsLocalization.eq_mk'_iff_mul_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : M} {z : S} :
z = mk' S x y z * (algebraMap R S) y = (algebraMap R S) x
theorem IsLocalization.eq_mk'_of_mul_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : M} {z : R} (h : z * y = x) :
(algebraMap R S) z = mk' S x y
theorem IsLocalization.mk'_eq_iff_eq_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : M} {z : S} :
mk' S x y = z (algebraMap R S) x = z * (algebraMap R S) y
theorem IsLocalization.mk'_add_eq_iff_add_mul_eq_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : M} {z₁ z₂ : S} :
mk' S x y + z₁ = z₂ (algebraMap R S) x + z₁ * (algebraMap R S) y = z₂ * (algebraMap R S) y
theorem IsLocalization.mk'_pow {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) (n : ) :
mk' S (x ^ n) (y ^ n) = mk' S x y ^ n
theorem IsLocalization.mk'_surjective {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) :
∃ (x : R) (y : M), mk' S x y = z
noncomputable def IsLocalization.fintype' {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] [Fintype R] :

The localization of a Fintype is a Fintype. Cannot be an instance.

Equations
def IsLocalization.uniqueOfZeroMem {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (h : 0 M) :

Localizing at a submonoid with 0 inside it leads to the trivial ring.

Equations
theorem IsLocalization.mk'_eq_iff_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x₁ x₂ : R} {y₁ y₂ : M} :
mk' S x₁ y₁ = mk' S x₂ y₂ (algebraMap R S) (y₂ * x₁) = (algebraMap R S) (y₁ * x₂)
theorem IsLocalization.mk'_eq_iff_eq' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x₁ x₂ : R} {y₁ y₂ : M} :
mk' S x₁ y₁ = mk' S x₂ y₂ (algebraMap R S) (x₁ * y₂) = (algebraMap R S) (x₂ * y₁)
theorem IsLocalization.eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : M} :
mk' S a₁ a₂ = mk' S b₁ b₂ ∃ (c : M), c * (b₂ * a₁) = c * (a₂ * b₁)
theorem IsLocalization.mk'_eq_zero_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (s : M) :
mk' S x s = 0 ∃ (m : M), m * x = 0
@[simp]
theorem IsLocalization.mk'_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : M) :
mk' S 0 s = 0
theorem IsLocalization.ne_zero_of_mk'_ne_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : M} (hxy : mk' S x y 0) :
x 0

Any localization of a commutative semiring without zero-divisors also has no zero-divisors.

theorem IsLocalization.sec_fst_ne_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : S} (hx : x 0) :
(sec M x).1 0
theorem IsLocalization.eq_iff_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] [Algebra R P] [IsLocalization M P] {x y : R} :
(algebraMap R S) x = (algebraMap R S) y (algebraMap R P) x = (algebraMap R P) y
theorem IsLocalization.mk'_eq_iff_mk'_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] [Algebra R P] [IsLocalization M P] {x₁ x₂ : R} {y₁ y₂ : M} :
mk' S x₁ y₁ = mk' S x₂ y₂ mk' P x₁ y₁ = mk' P x₂ y₂
theorem IsLocalization.mk'_eq_of_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : M} (H : a₂ * b₁ = b₂ * a₁) :
mk' S a₁ a₂ = mk' S b₁ b₂
theorem IsLocalization.mk'_eq_of_eq' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * a₂ = a₁ * b₂) :
mk' S a₁ a₂ = mk' S b₁ b₂
theorem IsLocalization.mk'_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : R) (b c : M) :
mk' S (a * c) (b * c) = mk' S a b
@[simp]
theorem IsLocalization.mk'_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} (hx : x M) :
mk' S x x, hx = 1
@[simp]
theorem IsLocalization.mk'_self' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : M} :
mk' S (↑x) x = 1
theorem IsLocalization.mk'_self'' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : M} :
mk' S (↑x) x = 1
theorem IsLocalization.mul_mk'_eq_mk'_of_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (z : M) :
(algebraMap R S) x * mk' S y z = mk' S (x * y) z
theorem IsLocalization.mk'_eq_mul_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
mk' S x y = (algebraMap R S) x * mk' S 1 y
@[simp]
theorem IsLocalization.mk'_mul_cancel_left {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
mk' S (y * x) y = (algebraMap R S) x
theorem IsLocalization.mk'_mul_cancel_right {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
mk' S (x * y) y = (algebraMap R S) x
@[simp]
theorem IsLocalization.mk'_mul_mk'_eq_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : M) :
mk' S (↑x) y * mk' S (↑y) x = 1
theorem IsLocalization.mk'_mul_mk'_eq_one' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) (h : x M) :
mk' S x y * mk' S y x, h = 1
theorem IsLocalization.smul_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (m : M) :
x mk' S y m = mk' S (x * y) m
@[simp]
theorem IsLocalization.smul_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (m : M) :
x mk' S 1 m = mk' S x m
@[simp]
theorem IsLocalization.smul_mk'_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {m : M} {r : R} :
m mk' S r m = (algebraMap R S) r
noncomputable instance IsLocalization.invertible_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : M) :
Invertible (mk' S 1 s)
Equations
@[simp]
theorem IsLocalization.invertible_mk'_one_invOf {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : M) :
(mk' S 1 s) = (algebraMap R S) s
theorem IsLocalization.isUnit_comp {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j : S →+* P) (y : M) :
IsUnit ((j.comp (algebraMap R S)) y)
theorem IsLocalization.eq_of_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) {x y : R} (h : (algebraMap R S) x = (algebraMap R S) y) :
g x = g y

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g(M) ⊆ Units P, f x = f y → g x = g y for all x y : R.

theorem IsLocalization.mk'_add {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : M) :
mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂
theorem IsLocalization.mul_add_inv_left {R : Type u_1} [CommSemiring R] {M : Submonoid R} {P : Type u_3} [CommSemiring P] {g : R →+* P} (h : ∀ (y : M), IsUnit (g y)) (y : M) (w z₁ z₂ : P) :
w * ((IsUnit.liftRight ((↑g).restrict M) h) y)⁻¹ + z₁ = z₂ w + g y * z₁ = g y * z₂
theorem IsLocalization.lift_spec_mul_add {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) (z : S) (w w' v : P) :
((toLocalizationMap M S).lift hg) z * w + w' = v g ((toLocalizationMap M S).sec z).1 * w + g ((toLocalizationMap M S).sec z).2 * w' = g ((toLocalizationMap M S).sec z).2 * v
noncomputable def IsLocalization.lift {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
S →+* P

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings 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
theorem IsLocalization.lift_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) (x : R) (y : M) :
(lift hg) (mk' S x y) = g x * ((IsUnit.liftRight ((↑g).restrict M) hg) y)⁻¹

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings 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.

theorem IsLocalization.lift_mk'_spec {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) (x : R) (v : P) (y : M) :
(lift hg) (mk' S x y) = v g x = g y * v
@[simp]
theorem IsLocalization.lift_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) (x : R) :
(lift hg) ((algebraMap R S) x) = g x
theorem IsLocalization.lift_eq_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) {x y : R × M} :
(lift hg) (mk' S x.1 x.2) = (lift hg) (mk' S y.1 y.2) g (x.1 * y.2) = g (y.1 * x.2)
@[simp]
theorem IsLocalization.lift_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
(lift hg).comp (algebraMap R S) = g
@[simp]
theorem IsLocalization.lift_of_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j : S →+* P) :
lift = j
theorem IsLocalization.monoidHom_ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] j k : S →* P (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) :
j = k

See note [partially-applied ext lemmas]

theorem IsLocalization.ringHom_ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] j k : S →+* P (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) :
j = k

See note [partially-applied ext lemmas]

theorem IsLocalization.ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j k : SP) (hj1 : j 1 = 1) (hk1 : k 1 = 1) (hjm : ∀ (a b : S), j (a * b) = j a * j b) (hkm : ∀ (a b : S), k (a * b) = k a * k b) (h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)) :
j = k

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

theorem IsLocalization.lift_unique {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) {j : S →+* P} (hj : ∀ (x : R), j ((algebraMap R S) x) = g x) :
lift hg = j
@[simp]
theorem IsLocalization.lift_id {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : S) :
(lift ) x = x
theorem IsLocalization.lift_surjective_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
Function.Surjective (lift hg) ∀ (v : P), ∃ (x : R × M), v * g x.2 = g x.1
theorem IsLocalization.lift_injective_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
Function.Injective (lift hg) ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y g x = g y
theorem IsLocalization.injective_iff_map_algebraMap_eq {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {T : Type u_4} [CommSemiring T] (f : S →+* T) :
Function.Injective f ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y f ((algebraMap R S) x) = f ((algebraMap R S) y)
noncomputable def IsLocalization.map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (g : R →+* P) (hy : M Submonoid.comap g T) :
S →+* Q

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
@[simp]
theorem IsLocalization.map_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (x : R) :
(map Q g hy) ((algebraMap R S) x) = (algebraMap P Q) (g x)
@[simp]
theorem IsLocalization.map_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) :
(map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g
theorem IsLocalization.map_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (x : R) (y : M) :
(map Q g hy) (mk' S x y) = mk' Q (g x) g y,
theorem IsLocalization.map_unique {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (j : S →+* Q) (hj : ∀ (x : R), j ((algebraMap R S) x) = (algebraMap P Q) (g x)) :
map Q g hy = j
theorem IsLocalization.map_comp_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) {A : Type u_5} [CommSemiring A] {U : Submonoid A} {W : Type u_6} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A} (hl : T Submonoid.comap l U) :
(map W l hl).comp (map Q g hy) = map W (l.comp 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.

theorem IsLocalization.map_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) {A : Type u_5} [CommSemiring A] {U : Submonoid A} {W : Type u_6} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A} (hl : T Submonoid.comap l U) (x : S) :
(map W l hl) ((map Q g hy) x) = (map W (l.comp g) ) x

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.

theorem IsLocalization.map_smul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (x : S) (z : R) :
(map Q g hy) (z x) = g z (map Q g hy) x
@[simp]
theorem IsLocalization.map_id_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {Q : Type u_5} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x : R) (y : M) :
(map Q (RingHom.id R) ) (mk' S x y) = mk' Q x y
@[simp]
theorem IsLocalization.map_id {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) (h : M Submonoid.comap (RingHom.id R) M := ) :
(map S (RingHom.id R) h) z = z
noncomputable def IsLocalization.ringEquivOfRingEquiv {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) :
S ≃+* Q

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
@[simp]
theorem IsLocalization.ringEquivOfRingEquiv_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : S) :
(ringEquivOfRingEquiv S Q h H) a = (map Q h ) a
@[simp]
theorem IsLocalization.ringEquivOfRingEquiv_symm_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : Q) :
(ringEquivOfRingEquiv S Q h H).symm a = (map S h.symm ) a
theorem IsLocalization.ringEquivOfRingEquiv_eq_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) :
(ringEquivOfRingEquiv S Q j H) = map Q j
theorem IsLocalization.ringEquivOfRingEquiv_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) :
(ringEquivOfRingEquiv S Q j H) ((algebraMap R S) x) = (algebraMap P Q) (j x)
theorem IsLocalization.ringEquivOfRingEquiv_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) (y : M) :
(ringEquivOfRingEquiv S Q j H) (mk' S x y) = mk' Q (j x) j y,
@[simp]
theorem IsLocalization.ringEquivOfRingEquiv_symm {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j M = T) :
theorem IsLocalization.map_injective_of_injective {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (h : Function.Injective g) [IsLocalization (Submonoid.map g M) Q] :
Function.Injective (map Q g )

Injectivity of a map descends to the map induced on localizations.

theorem IsLocalization.map_surjective_of_surjective {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (h : Function.Surjective g) [IsLocalization (Submonoid.map g M) Q] :

Surjectivity of a map descends to the map induced on localizations.

Constructing a localization at a given submonoid #

theorem Localization.add_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (a : R) (b : M) (c : R) (d : M) :
mk a b + mk c d = mk (b * c + d * a) (b * d)
theorem Localization.add_mk_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} (a : R) (b : M) (c : R) :
mk a b + mk c b = mk (a + c) b
def Localization.mkAddMonoidHom {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : M) :

For any given denominator b : M, the map a ↦ a / b is an AddMonoidHom from R to Localization M.

Equations
@[simp]
theorem Localization.mkAddMonoidHom_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : M) (a : R) :
(mkAddMonoidHom b) a = mk a b
theorem Localization.mk_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} {ι : Type u_4} (f : ιR) (s : Finset ι) (b : M) :
mk (∑ is, f i) b = is, mk (f i) b
theorem Localization.mk_list_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : List R) (b : M) :
mk l.sum b = (List.map (fun (a : R) => mk a b) l).sum
theorem Localization.mk_multiset_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : Multiset R) (b : M) :
mk l.sum b = (Multiset.map (fun (a : R) => mk a b) l).sum
theorem Localization.mk_one_eq_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) :
mk x 1 = (algebraMap R (Localization M)) x
theorem Localization.mk_eq_mk'_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) (y : M) :
theorem Localization.mk_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} {A : Type u_4} [CommSemiring A] [Algebra A R] (m : A) :
mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m
theorem Localization.neg_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a : R) (b : M) :
-mk a b = mk (-a) b
theorem Localization.sub_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a c : R) (b d : M) :
mk a b - mk c d = mk (d * a - b * c) (b * d)
theorem IsLocalization.mk'_neg {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (x : R) (y : M) :
mk' S (-x) y = -mk' S x y
theorem IsLocalization.mk'_sub {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : M) :
mk' S (x₁ * y₂ - x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
theorem IsLocalization.injective_of_map_algebraMap_zero {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {T : Type u_5} [CommRing T] (f : S →+* T) (h : ∀ (x : R), f ((algebraMap R S) x) = 0(algebraMap R S) x = 0) :
theorem IsLocalization.to_map_eq_zero_iff {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {x : R} (hM : M nonZeroDivisors R) :
(algebraMap R S) x = 0 x = 0
theorem IsLocalization.injective {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (hM : M nonZeroDivisors R) :
theorem IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] [Nontrivial R] (hM : M nonZeroDivisors R) {x : R} (hx : x nonZeroDivisors R) :
(algebraMap R S) x 0
theorem IsLocalization.sec_snd_ne_zero {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] [Nontrivial R] (hM : M nonZeroDivisors R) (x : S) :
(sec M x).2 0
@[deprecated IsLocalization.noZeroDivisors (since := "2025-03-18")]

Alias of IsLocalization.noZeroDivisors.


Any localization of a commutative semiring without zero-divisors also has no 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.