mathlib documentation

ring_theory.localization

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, 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 #

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

theorem is_localization.of_le {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (N : submonoid R) (h₁ : M N) (h₂ : ∀ (r : R), r Nis_unit ((algebra_map R S) r)) :
def is_localization.to_localization_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

is_localization.to_localization_map M S shows S is the monoid localization of R at M.

Equations
@[simp]
def is_localization.is_integer (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] (a : S) :
Prop

Given a : S, S a localization of R, is_integer R a iff a is in the image of the localization map from R to S.

Equations
theorem is_localization.is_integer_zero {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :
theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :
theorem is_localization.is_integer_add {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a b : S} (ha : is_localization.is_integer R a) (hb : is_localization.is_integer R b) :
theorem is_localization.is_integer_mul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a b : S} (ha : is_localization.is_integer R a) (hb : is_localization.is_integer R b) :
theorem is_localization.is_integer_smul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a : R} {b : S} (hb : is_localization.is_integer R b) :
theorem is_localization.exists_integer_multiple' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (a : 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.

theorem is_localization.exists_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (a : S) :

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.

noncomputable def is_localization.sec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization 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 is_localization.sec_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :

Given z : S, is_localization.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 is_localization.sec_spec' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :

Given z : S, is_localization.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 is_localization.exist_integer_multiples {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) :
∃ (b : M), ∀ (i : ι), i sis_localization.is_integer R (b f i)

We can clear the denominators of a finset-indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_fintype {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} [fintype ι] (f : ι → S) :
∃ (b : M), ∀ (i : ι), is_localization.is_integer R (b f i)

We can clear the denominators of a fintype-indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (s : finset S) :
∃ (b : M), ∀ (a : S), a sis_localization.is_integer R (b a)

We can clear the denominators of a finite set of fractions.

noncomputable def is_localization.common_denom {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) :

A choice of a common multiple of the denominators of a finset-indexed family of fractions.

Equations
noncomputable def is_localization.integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : s) :
R

The numerator of a fraction after clearing the denominators of a finset-indexed family of fractions.

Equations
@[simp]
theorem is_localization.map_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : s) :
noncomputable def is_localization.common_denom_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (s : finset S) :

A choice of a common multiple of the denominators of a finite set of fractions.

Equations
noncomputable def is_localization.finset_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] [decidable_eq R] (s : finset S) :

The finset of numerators after clearing the denominators of a finite set of fractions.

Equations
theorem is_localization.map_right_cancel {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x y : R} {c : M} (h : (algebra_map R S) ((c) * x) = (algebra_map R S) ((c) * y)) :
theorem is_localization.map_left_cancel {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x y : R} {c : M} (h : (algebra_map R S) (x * c) = (algebra_map R S) (y * c)) :
theorem is_localization.eq_zero_of_fst_eq_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {z : S} {x : R} {y : M} (h : z * (algebra_map R S) y = (algebra_map R S) x) (hx : x = 0) :
z = 0
theorem is_localization.map_eq_zero_iff {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (r : R) :
(algebra_map R S) r = 0 ∃ (m : M), r * m = 0
noncomputable def is_localization.mk' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
S

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

Equations
@[simp]
theorem is_localization.mk'_sec {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (z : S) :
theorem is_localization.mk'_mul {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x₁ x₂ : R) (y₁ y₂ : M) :
is_localization.mk' S (x₁ * x₂) (y₁ * y₂) = (is_localization.mk' S x₁ y₁) * is_localization.mk' S x₂ y₂
theorem is_localization.mk'_one {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x : R) :
@[simp]
theorem is_localization.mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_spec' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_spec_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x y : R) (hy : y M) :
(is_localization.mk' S x y, hy⟩) * (algebra_map R S) y = (algebra_map R S) x
@[simp]
theorem is_localization.mk'_spec'_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (x y : R) (hy : y M) :
((algebra_map R S) y) * is_localization.mk' S x y, hy⟩ = (algebra_map R S) x
theorem is_localization.eq_mk'_iff_mul_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x : R} {y : M} {z : S} :
theorem is_localization.mk'_eq_iff_eq_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x : R} {y : M} {z : S} :
theorem is_localization.mk'_surjective {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :
∃ (x : R) (y : M), is_localization.mk' S x y = z
theorem is_localization.mk'_eq_iff_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x₁ x₂ : R} {y₁ y₂ : M} :
is_localization.mk' S x₁ y₁ = is_localization.mk' S x₂ y₂ (algebra_map R S) (x₁ * y₂) = (algebra_map R S) (x₂ * y₁)
theorem is_localization.mk'_mem_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x : R} {y : M} {I : ideal S} :
@[protected]
theorem is_localization.eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {a₁ b₁ : R} {a₂ b₂ : M} :
is_localization.mk' S a₁ a₂ = is_localization.mk' S b₁ b₂ ∃ (c : M), (a₁ * b₂) * c = (b₁ * a₂) * c
theorem is_localization.eq_iff_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] [algebra R P] [is_localization M P] {x y : R} :
theorem is_localization.mk'_eq_iff_mk'_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] [algebra R P] [is_localization M P] {x₁ x₂ : R} {y₁ y₂ : M} :
is_localization.mk' S x₁ y₁ = is_localization.mk' S x₂ y₂ is_localization.mk' P x₁ y₁ = is_localization.mk' P x₂ y₂
theorem is_localization.mk'_eq_of_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * a₂ = a₁ * b₂) :
is_localization.mk' S a₁ a₂ = is_localization.mk' S b₁ b₂
@[simp]
theorem is_localization.mk'_self {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {x : R} (hx : x M) :
is_localization.mk' S x x, hx⟩ = 1
@[simp]
theorem is_localization.mk'_self' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {x : M} :
theorem is_localization.mk'_self'' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {x : M} :
theorem is_localization.mul_mk'_eq_mk'_of_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x y : R) (z : M) :
theorem is_localization.mk'_eq_mul_mk'_one {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_mul_cancel_left {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem is_localization.mk'_mul_cancel_right {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_mul_mk'_eq_one {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x y : M) :
theorem is_localization.mk'_mul_mk'_eq_one' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) (h : x M) :
theorem is_localization.is_unit_comp {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (j : S →+* P) (y : M) :
theorem is_localization.eq_of_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {x y : R} (h : (algebra_map R S) x = (algebra_map R S) y) :
g x = g 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.

theorem is_localization.mk'_add {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x₁ x₂ : R) (y₁ y₂ : M) :
is_localization.mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = is_localization.mk' S x₁ y₁ + is_localization.mk' S x₂ y₂
noncomputable def is_localization.lift {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
S →+* P

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
theorem is_localization.lift_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) (y : M) :

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.

theorem is_localization.lift_mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) (v : P) (y : M) :
@[simp]
theorem is_localization.lift_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) :
theorem is_localization.lift_eq_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {x y : R × M} :
@[simp]
theorem is_localization.lift_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
@[simp]
theorem is_localization.lift_of_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (j : S →+* P) :
theorem is_localization.monoid_hom_ext {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] ⦃j k : S →* P⦄ (h : j.comp (algebra_map R S) = k.comp (algebra_map R S)) :
j = k

See note [partially-applied ext lemmas]

theorem is_localization.ring_hom_ext {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] ⦃j k : S →+* P⦄ (h : j.comp (algebra_map R S) = k.comp (algebra_map R S)) :
j = k

See note [partially-applied ext lemmas]

@[protected]
theorem is_localization.ext {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (j k : S → P) (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 ((algebra_map R S) a) = k ((algebra_map 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 is_localization.lift_unique {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {j : S →+* P} (hj : ∀ (x : R), j ((algebra_map R S) x) = g x) :
@[simp]
theorem is_localization.lift_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : S) :
theorem is_localization.lift_surjective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
function.surjective (is_localization.lift hg) ∀ (v : P), ∃ (x : R × M), v * g (x.snd) = g x.fst
theorem is_localization.lift_injective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
noncomputable def is_localization.map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization 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 algebra_map P Q (g x) * (algebra_map P Q (g y))⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations
theorem is_localization.map_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] (x : R) :
@[simp]
theorem is_localization.map_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] :
theorem is_localization.map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] (x : R) (y : M) :
@[simp]
theorem is_localization.map_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) (h : M submonoid.comap (ring_hom.id R) M := _) :
theorem is_localization.map_unique {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] (j : S →+* Q) (hj : ∀ (x : R), j ((algebra_map R S) x) = (algebra_map P Q) (g x)) :
theorem is_localization.map_comp_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] {A : Type u_5} [comm_ring A] {U : submonoid A} {W : Type u_6} [comm_ring W] [algebra A W] [is_localization U W] {l : P →+* A} (hl : T submonoid.comap l U) :

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.

theorem is_localization.map_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] {A : Type u_5} [comm_ring A] {U : submonoid A} {W : Type u_6} [comm_ring W] [algebra A W] [is_localization U W] {l : P →+* A} (hl : T submonoid.comap l U) (x : S) :

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.

@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom M = T) (ᾰ : S) :
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_symm_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom M = T) (ᾰ : Q) :
noncomputable def is_localization.ring_equiv_of_ring_equiv {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom 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
theorem is_localization.ring_equiv_of_ring_equiv_eq_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) :
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) :
theorem is_localization.ring_equiv_of_ring_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) (y : M) :
noncomputable def is_localization.alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] :

If S, Q are localizations of R at the submonoid M respectively, there is an isomorphism of localizations S ≃ₐ[R] Q.

Equations
@[simp]
theorem is_localization.alg_equiv_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] (ᾰ : S) :
@[simp]
theorem is_localization.alg_equiv_symm_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] (ᾰ : Q) :
@[simp]
theorem is_localization.alg_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_ring Q] [algebra R Q] [is_localization M Q] (x : R) (y : M) :
@[simp]
theorem is_localization.alg_equiv_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_ring Q] [algebra R Q] [is_localization M Q] (x : R) (y : M) :
theorem is_localization.is_localization_of_alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [algebra R P] [is_localization M S] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [algebra R P] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (h : S ≃+* P) :
theorem is_localization.is_localization_of_base_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (h : R ≃+* P) :
theorem is_localization.is_localization_iff_of_base_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
def is_localization.away {R : Type u_1} [comm_ring R] (x : R) (S : Type u_2) [comm_ring S] [algebra R S] :
Prop

Given x : R, the typeclass is_localization.away x S states that S is isomorphic to the localization of R at the submonoid generated by x.

noncomputable def is_localization.away.inv_self {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] (x : R) [is_localization.away x S] :
S

Given x : R and a localization map F : R →+* S away from x, inv_self is (F x)⁻¹.

Equations
noncomputable def is_localization.away.lift {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (g x)) :
S →+* P

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
@[simp]
theorem is_localization.away.away_map.lift_eq {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (g x)) (a : R) :
@[simp]
theorem is_localization.away.away_map.lift_comp {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (g x)) :
noncomputable def is_localization.away.away_to_away_right {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] (y : R) [algebra R P] [is_localization.away (x * y) P] :
S →+* P

Given x y : R and localizations S, P away from x and x * y respectively, the homomorphism induced from S to P.

Equations
noncomputable def is_localization.away.map {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (Q : Type u_4) [comm_ring Q] [algebra P Q] (f : R →+* P) (r : R) [is_localization.away r S] [is_localization.away (f r) Q] :
S →+* Q

Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

Equations
def is_localization.inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] :

The submonoid of S = M⁻¹R consisting of { 1 / x | x ∈ M }.

Equations
noncomputable def is_localization.equiv_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

There is an equivalence of monoids between the image of M and inv_submonoid.

noncomputable def is_localization.to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

There is a canonical map from M to inv_submonoid sending x to 1 / x.

Equations
@[simp]
theorem is_localization.to_inv_submonoid_mul {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : M) :
@[simp]
theorem is_localization.mul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : M) :
@[simp]
theorem is_localization.smul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : M) :
theorem is_localization.surj' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :
∃ (r : R) (m : M), z = r ((is_localization.to_inv_submonoid M S) m)
theorem is_localization.to_inv_submonoid_eq_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : M) :
theorem is_localization.mem_inv_submonoid_iff_exists_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : S) :
theorem is_localization.finite_type_of_monoid_fg {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] [monoid.fg M] :

Constructing a localization at a given submonoid #

@[protected]
def localization.add {R : Type u_1} [comm_ring R] {M : submonoid R} (z w : localization M) :

Addition in a ring localization is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨b * c + d * a, b * d⟩.

Should not be confused with add_localization.add, which is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩.

Equations
@[protected, instance]
def localization.has_add {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
theorem localization.add_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (a : R) (b : M) (c : R) (d : M) :
theorem localization.add_mk_self {R : Type u_1} [comm_ring R] {M : submonoid R} (a : R) (b : M) (c : R) :
@[protected]
def localization.neg {R : Type u_1} [comm_ring R] {M : submonoid R} (z : localization M) :

Negation in a ring localization is defined as -⟨a, b⟩ = ⟨-a, b⟩.

Equations
@[protected, instance]
def localization.has_neg {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
theorem localization.neg_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (a : R) (b : M) :
@[protected]
def localization.zero {R : Type u_1} [comm_ring R] {M : submonoid R} :

The zero element in a ring localization is defined as ⟨0, 1⟩.

Should not be confused with add_localization.zero which is ⟨0, 0⟩.

Equations
@[protected, instance]
def localization.has_zero {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
theorem localization.mk_zero {R : Type u_1} [comm_ring R] {M : submonoid R} (b : M) :
@[protected, instance]
def localization.distrib_mul_action {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] :
Equations
@[protected, instance]
def localization.algebra {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra S R] :
Equations
@[protected, instance]
theorem localization.mk_one_eq_algebra_map {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) :
theorem localization.mk_eq_mk'_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) (y : M) :
noncomputable def localization.alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

The localization of R at M as a quotient type is isomorphic to any other localization.

Equations
@[simp]
theorem localization.alg_equiv_symm_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (ᾰ : S) :
@[simp]
theorem localization.alg_equiv_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (ᾰ : localization M) :
@[simp]
theorem localization.alg_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem localization.alg_equiv_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem localization.alg_equiv_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem localization.alg_equiv_symm_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
noncomputable def localization.away_lift {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (f : R →+* P) (r : R) (hr : is_unit (f r)) :

Given a map f : R →+* S and an element r : R, such that f r is invertible, we may construct a map Rᵣ →+* S.

noncomputable def localization.away_map {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (f : R →+* P) (r : R) :

Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

def ideal.prime_compl {R : Type u_1} [comm_ring R] (I : ideal R) [hp : I.is_prime] :

The complement of a prime ideal I ⊆ R is a submonoid of R.

Equations
@[protected]
def is_localization.at_prime {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hp : I.is_prime] :
Prop

Given a prime ideal P, the typeclass is_localization.at_prime S P states that S is isomorphic to the localization of R at the complement of P.

@[protected]
def localization.at_prime {R : Type u_1} [comm_ring R] (I : ideal R) [hp : I.is_prime] :
Type u_1

Given a prime ideal P, localization.at_prime S P is a localization of R at the complement of P, as a quotient type.

theorem is_localization.at_prime.local_ring {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hp : I.is_prime] [is_localization.at_prime S I] :
@[protected, instance]

The localization of R at the complement of a prime ideal is a local ring.

theorem is_localization.mem_map_algebra_map_iff {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {I : ideal R} {z : S} :
z ideal.map (algebra_map R S) I ∃ (x : I × M), z * (algebra_map R S) (x.snd) = (algebra_map R S) (x.fst)
theorem is_localization.map_comap {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (J : ideal S) :
theorem is_localization.comap_map_of_is_prime_disjoint {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (I : ideal R) (hI : I.is_prime) (hM : disjoint M I) :
def is_localization.order_embedding {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

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

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

theorem is_localization.is_prime_of_is_prime_disjoint {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (I : ideal R) (hp : I.is_prime) (hd : disjoint M I) :

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

def is_localization.order_iso_of_prime {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :
{p // p.is_prime} ≃o {p // p.is_prime disjoint M p}

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

Equations

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

noncomputable def is_localization.at_units (R : Type u_1) [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (H : ∀ (x : M), is_unit x) :

The localization at a module of units is isomorphic to the ring

Equations
noncomputable def is_localization.at_unit (R : Type u_1) [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (x : R) (e : is_unit x) [is_localization.away x S] :

The localization away from a unit is isomorphic to the ring

Equations
noncomputable def is_localization.at_one (R : Type u_1) [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] [is_localization.away 1 S] :

The localization at one is isomorphic to the ring.

Equations
@[nolint]
def is_localization.localization_localization_submodule {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (N : submonoid S) :

Localizing wrt M ⊆ R and then wrt N ⊆ S = M⁻¹R is equal to the localization of R wrt this module. See localization_localization_is_localization.

Equations
@[simp]
theorem is_localization.mem_localization_localization_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {N : submonoid S} {x : R} :
theorem is_localization.localization_localization_surj {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (N : submonoid S) (T : Type u_4) [comm_ring T] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization N T] (x : T) :
theorem is_localization.localization_localization_eq_iff_exists {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (N : submonoid S) (T : Type u_4) [comm_ring T] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization N T] (x y : R) :

Given submodules M ⊆ R and N ⊆ S = M⁻¹R, with f : R →+* S the localization map, we have N ⁻¹ S = T = (f⁻¹ (N • f(M))) ⁻¹ R. I.e., the localization of a localization is a localization.

theorem is_localization.localization_localization_is_localization_of_has_all_units {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (N : submonoid S) (T : Type u_4) [comm_ring T] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization N T] (H : ∀ (x : S), is_unit xx N) :

Given submodules M ⊆ R and N ⊆ S = M⁻¹R, with f : R →+* S the localization map, if N contains all the units of S, then N ⁻¹ S = T = (f⁻¹ N) ⁻¹ R. I.e., the localization of a localization is a localization.

Given a submodule M ⊆ R and a prime ideal p of S = M⁻¹R, with f : R →+* S the localization map, then T = Sₚ is the localization of R at f⁻¹(p).

Given a submodule M ⊆ R and a prime ideal p of M⁻¹R, with f : R →+* S the localization map, then (M⁻¹R)ₚ is isomorphic (as an R-algebra) to the localization of R at f⁻¹(p).

Equations
noncomputable def is_localization.localization_algebra_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (T : Type u_4) [comm_ring T] [algebra R T] (M N : submonoid R) (h : M N) [is_localization M S] [is_localization N T] :

Given submonoids M ≤ N of R, this is the canonical algebra structure of M⁻¹S acting on N⁻¹S.

Equations
theorem is_localization.localization_is_scalar_tower_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (T : Type u_4) [comm_ring T] [algebra R T] (M N : submonoid R) (h : M N) [is_localization M S] [is_localization N T] :

If M ≤ N are submonoids of R, then the natural map M⁻¹S →+* N⁻¹S commutes with the localization maps

theorem is_localization.is_localization_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (T : Type u_4) [comm_ring T] [algebra R T] (M N : submonoid R) (h : M N) [is_localization M S] [is_localization N T] [algebra S T] [is_scalar_tower R S T] :

If M ≤ N are submonoids of R, then N⁻¹S is also the localization of M⁻¹S at N.

theorem is_localization.is_localization_of_is_exists_mul_mem {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (M N : submonoid R) [is_localization M S] (h : M N) (h' : ∀ (x : N), ∃ (m : R), m * x M) :

If M ≤ N are submonoids of R such that ∀ x : N, ∃ m : R, m * x ∈ M, then the localization at N is equal to the localizaton of M.

def is_localization.coe_submodule {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) :

Map from ideals of R to submodules of S induced by f.

Equations
theorem is_localization.mem_coe_submodule {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) {x : S} :
x is_localization.coe_submodule S I ∃ (y : R), y I (algebra_map R S) y = x
theorem is_localization.coe_submodule_mono {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] {I J : ideal R} (h : I J) :
@[simp]
theorem is_localization.coe_submodule_bot {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] :
@[simp]
theorem is_localization.coe_submodule_top {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] :
@[simp]
theorem is_localization.coe_submodule_span {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (s : set R) :
@[simp]
theorem is_localization.coe_submodule_span_singleton {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (x : R) :
theorem is_localization.map_smul {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} {T : submonoid P} (hy : M submonoid.comap g T) {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] (x : S) (z : R) :
theorem is_localization.is_noetherian_ring {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (h : is_noetherian_ring R) :
noncomputable def is_localization.coeff_integer_normalization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (p : polynomial S) (i : ) :
R

coeff_integer_normalization p gives the coefficients of the polynomial integer_normalization p

Equations
noncomputable def is_localization.integer_normalization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (p : polynomial S) :

integer_normalization g normalizes g to have integer coefficients by clearing the denominators

Equations
theorem is_localization.integer_normalization_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (p : polynomial S) :
∃ (b : M), ∀ (i : ), (algebra_map R S) ((is_localization.integer_normalization M p).coeff i) = b p.coeff i
theorem is_localization.integer_normalization_eval₂_eq_zero {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {R' : Type u_5} [comm_ring R'] (g : S →+* R') (p : polynomial S) {x : R'} (hx : polynomial.eval₂ g x p = 0) :
theorem is_localization.integer_normalization_aeval_eq_zero {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {R' : Type u_5} [comm_ring R'] [algebra R R'] [algebra S R'] [is_scalar_tower R S R'] (p : polynomial S) {x : R'} (hx : (polynomial.aeval x) p = 0) :
theorem is_localization.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {x : R} (hM : M R) :
(algebra_map R S) x = 0 x = 0
@[protected]
theorem is_localization.injective {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (hM : M R) :
@[protected]
theorem is_localization.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] [nontrivial R] (hM : M R) {x : R} (hx : x R) :
theorem is_localization.map_injective_of_injective {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (Q : Type u_4) [comm_ring Q] [algebra P Q] (hg : function.injective g) [is_localization (submonoid.map g M) Q] (hM : submonoid.map g M P) :

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

theorem is_localization.is_domain_of_le_non_zero_divisors (S : Type u_2) [comm_ring S] {A : Type u_6} [comm_ring A] [is_domain A] [algebra A S] {M : submonoid A} [is_localization M S] (hM : M A) :

A comm_ring S which is the localization of an integral domain R at a subset of non-zero elements is an integral domain. See note [reducible non-instances].

theorem is_localization.is_domain_localization {A : Type u_6} [comm_ring A] [is_domain A] {M : submonoid A} (hM : M A) :

The localization at of an integral domain to a set of non-zero elements is an integral domain. See note [reducible non-instances].

@[protected, instance]

The localization of an integral domain at the complement of a prime ideal is an integral domain.

theorem is_localization.at_prime.is_unit_to_map_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) :
theorem is_localization.at_prime.to_map_mem_maximal_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (h : local_ring S := _) :
theorem is_localization.at_prime.is_unit_mk'_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (y : (I.prime_compl)) :
theorem is_localization.at_prime.mk'_mem_maximal_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (y : (I.prime_compl)) (h : local_ring S := _) :

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

theorem localization.le_comap_prime_compl_iff {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] {I : ideal R} [hI : I.is_prime] {J : ideal P} [hJ : J.is_prime] {f : R →+* P} :
noncomputable def localization.local_ring_hom {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) :

For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the localization of R at J.comap f to the localization of S at J.

To make this definition more flexible, we allow any ideal I of R as input, together with a proof that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.

Equations
theorem localization.local_ring_hom_to_map {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) (x : R) :
theorem localization.local_ring_hom_mk' {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) (x : R) (y : (I.prime_compl)) :
@[protected, instance]
def localization.is_local_ring_hom_local_ring_hom {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) :
theorem localization.local_ring_hom_unique {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) {j : localization.at_prime I →+* localization.at_prime J} (hj : ∀ (x : R), j ((algebra_map R (localization.at_prime I)) x) = (algebra_map P (localization.at_prime J)) (f x)) :
@[simp]
theorem localization.local_ring_hom_comp {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] {S : Type u_2} [comm_ring S] (J : ideal S) [hJ : J.is_prime] (K : ideal P) [hK : K.is_prime] (f : R →+* S) (hIJ : I = ideal.comap f J) (g : S →+* P) (hJK : J = ideal.comap g K) :
theorem localization_map_bijective_of_field {R : Type u_1} {Rₘ : Type u_2} [comm_ring R] [is_domain R] [comm_ring Rₘ] {M : submonoid R} (hM : 0 M) (hR : is_field R) [algebra R Rₘ] [is_localization M Rₘ] :

If R is a field, then localizing at a submonoid not containing 0 adds no new elements.

def is_fraction_ring (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] :
Prop

is_fraction_ring R K states K is the field of fractions of an integral domain R.

@[protected, instance]

The cast from int to rat as a fraction_ring.

theorem is_fraction_ring.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] {x : R} :
(algebra_map R K) x = 0 x = 0
@[protected]
theorem is_fraction_ring.injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] [is_fraction_ring R K] :
@[protected, instance]
@[protected]
theorem is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] [nontrivial R] {x : R} (hx : x R) :
@[protected]
theorem is_fraction_ring.is_domain (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :

A comm_ring K which is the localization of an integral domain R at R - {0} is an integral domain.

@[protected]
noncomputable def is_fraction_ring.inv (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] (z : K) :
K

The inverse of an element in the field of fractions of an integral domain.

Equations
@[protected]
theorem is_fraction_ring.mul_inv_cancel (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] (x : K) (hx : x 0) :
noncomputable def is_fraction_ring.to_field (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :

A comm_ring K which is the localization of an integral domain R at R - {0} is a field. See note [reducible non-instances].

Equations
theorem is_fraction_ring.mk'_mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r s : A} (hs : s A) :
@[simp]
theorem is_fraction_ring.mk'_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r : A} (s : A) :
theorem is_fraction_ring.div_surjective {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] (z : K) :
∃ (x y : A) (hy : y A), (algebra_map A K) x / (algebra_map A K) y = z
theorem is_fraction_ring.is_unit_map_of_injective {A : Type u_4} [comm_ring A] [is_domain A] {L : Type u_7} [field L] {g : A →+* L} (hg : function.injective g) (y : A) :
noncomputable def is_fraction_ring.lift {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) :
K →+* L

Given an integral domain A with field of fractions 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
@[simp]
theorem is_fraction_ring.lift_algebra_map {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) (x : A) :

Given an integral domain A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, the field hom induced from K to L maps x to g x for all x : A.

theorem is_fraction_ring.lift_mk' {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) (x : A) (y : A) :

Given an integral domain A with field of fractions 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.

noncomputable def is_fraction_ring.map {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} {B : Type u_6} [comm_ring B] [is_domain B] [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra B L] [is_fraction_ring B L] {j : A →+* B} (hj : function.injective j) :
K →+* L

Given integral domains A, B with fields of fractions K, 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
noncomputable def is_fraction_ring.field_equiv_of_ring_equiv {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} {B : Type u_6} [comm_ring B] [is_domain B] [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra B L] [is_fraction_ring B L] (h : A ≃+* B) :
K ≃+* L

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
theorem is_fraction_ring.is_algebraic_iff (A : Type u_4) [comm_ring A] [is_domain A] (K : Type u_5) [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra A L] [algebra K L] [is_scalar_tower A K L] {x : L} :

An element of a field is algebraic over the ring A iff it is algebraic over the field of fractions of A.

theorem is_fraction_ring.comap_is_algebraic_iff {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra A L] [algebra K L] [is_scalar_tower A K L] :

A field is algebraic over the ring A iff it is algebraic over the field of fractions of A.

theorem is_fraction_ring.exists_reduced_fraction (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] (x : K) :
∃ (a : A) (b : A), (∀ {d : A}, d ad bis_unit d) is_localization.mk' K a b = x
noncomputable def is_fraction_ring.num (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] (x : K) :
A

f.num x is the numerator of x : f.codomain as a reduced fraction.

Equations
noncomputable def is_fraction_ring.denom (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] (x : K) :

f.num x is the denominator of x : f.codomain as a reduced fraction.

Equations
theorem is_fraction_ring.num_denom_reduced (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] (x : K) {d : A} :
@[simp]
theorem is_fraction_ring.eq_zero_of_num_eq_zero {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] {x : K} (h : is_fraction_ring.num A x = 0) :
x = 0
theorem is_fraction_ring.is_fraction_ring_iff_of_base_ring_equiv {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
noncomputable def localization_algebra {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] :
algebra Rₘ Sₘ

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
theorem algebra_map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [