mathlib3 documentation

ring_theory.localization.basic

Localizations of commutative rings #

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

We characterize the localization of a commutative ring R at a submonoid M up to isomorphism; that is, a commutative ring S is the localization of R at M iff we can find a ring homomorphism f : R →+* S satisfying 3 properties:

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

In the following, let R, P be commutative rings, S, Q be R- and P-algebras and M, T be submonoids of R and P respectively, e.g.:

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

Main definitions #

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

@[class]
structure is_localization {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] :
Prop

The typeclass is_localization (M : submodule R) S where S is an R-algebra expresses that S is isomorphic to the localization of R at M.

Instances of this typeclass
theorem is_localization.of_le {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (N : submonoid R) (h₁ : M N) (h₂ : (r : R), r N is_unit ((algebra_map R S) r)) :
@[reducible]

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

noncomputable def is_localization.sec {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring 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_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring 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_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring 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.map_right_cancel {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (r : R) :
(algebra_map R S) r = 0 (m : M), m * r = 0
noncomputable def is_localization.mk' {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring 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'_mul {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring 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_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (x : R) :
@[simp]
theorem is_localization.mk'_spec {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_spec' {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem is_localization.mk'_spec_mk {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (x y : R) (hy : y M) :
@[simp]
theorem is_localization.mk'_spec'_mk {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (x y : R) (hy : y M) :
theorem is_localization.eq_mk'_iff_mul_eq {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {x : R} {y : M} {z : S} :
theorem is_localization.mk'_add_eq_iff_add_mul_eq_mul {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {x : R} {y : M} {z₁ z₂ : S} :
is_localization.mk' S x y + z₁ = z₂ (algebra_map R S) x + z₁ * (algebra_map R S) y = z₂ * (algebra_map R S) y
theorem is_localization.mk'_surjective {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (z : S) :
(x : R) (y : M), is_localization.mk' S x y = z
noncomputable def is_localization.fintype' {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] [fintype R] :

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

Equations
def is_localization.unique_of_zero_mem {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (h : 0 M) :

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

Equations
theorem is_localization.mk'_eq_iff_eq {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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) (y₂ * x₁) = (algebra_map R S) (y₁ * x₂)
theorem is_localization.mk'_eq_iff_eq' {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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), c * (b₂ * a₁) = c * (a₂ * b₁)
theorem is_localization.mk'_eq_zero_iff {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (x : R) (s : M) :
is_localization.mk' S x s = 0 (m : M), m * x = 0
@[simp]
theorem is_localization.mk'_zero {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (s : M) :
theorem is_localization.ne_zero_of_mk'_ne_zero {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {x : R} {y : M} (hxy : is_localization.mk' S x y 0) :
x 0
theorem is_localization.eq_iff_eq {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {a₁ b₁ : R} {a₂ b₂ : M} (H : a₂ * b₁ = b₂ * a₁) :
is_localization.mk' S a₁ a₂ = is_localization.mk' S b₁ b₂
theorem is_localization.mk'_eq_of_eq' {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring 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_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] {x : M} :
theorem is_localization.mk'_self'' {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] {x : M} :
theorem is_localization.mul_mk'_eq_mk'_of_mul {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem is_localization.mk'_mul_cancel_right {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] (j : S →+* P) (y : M) :
theorem is_localization.eq_of_eq {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semirings 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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₂
theorem is_localization.mul_add_inv_left {R : Type u_1} [comm_semiring R] {M : submonoid R} {P : Type u_3} [comm_semiring P] {g : R →+* P} (h : (y : M), is_unit (g y)) (y : M) (w z₁ z₂ : P) :
w * ((is_unit.lift_right (g.to_monoid_hom.restrict M) h) y)⁻¹ + z₁ = z₂ w + g y * z₁ = g y * z₂
noncomputable def is_localization.lift {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semirings 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semirings 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] (j : S →+* P) :
theorem is_localization.monoid_hom_ext {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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.alg_hom_subsingleton {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] [algebra R P] :
@[protected]
theorem is_localization.ext {R : Type u_1} [comm_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (x : S) :
theorem is_localization.lift_surjective_iff {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} (hg : (y : M), is_unit (g y)) :
theorem is_localization.lift_injective_iff {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] :
theorem is_localization.map_mk' {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] {A : Type u_5} [comm_semiring A] {U : submonoid A} {W : Type u_6} [comm_semiring W] [algebra A W] [is_localization U W] {l : P →+* A} (hl : T submonoid.comap l U) :

If comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] {A : Type u_5} [comm_semiring A] {U : submonoid A} {W : Type u_6} [comm_semiring W] [algebra A W] [is_localization U W] {l : P →+* A} (hl : T submonoid.comap l U) (x : S) :

If comm_semiring 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_smul {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_semiring Q] (hy : M submonoid.comap g T) [algebra P Q] [is_localization T Q] (x : S) (z : R) :
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_apply {R : Type u_1} [comm_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_semiring 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_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_semiring 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_semiring R] {M : submonoid R} (S : Type u_2) [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_semiring 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
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_eq {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_semiring 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_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_semiring 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_mk' {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_semiring 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_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_semiring 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_semiring R] (M : submonoid R) {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] [algebra R P] [is_localization M S] (h : S ≃ₐ[R] P) :

Constructing a localization at a given submonoid #

@[protected, instance]
Equations
@[protected, irreducible]
def localization.add {R : Type u_1} [comm_semiring 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]
Equations
theorem localization.add_mk {R : Type u_1} [comm_semiring R] {M : submonoid R} (a : R) (b : M) (c : R) (d : M) :
theorem localization.add_mk_self {R : Type u_1} [comm_semiring R] {M : submonoid R} (a : R) (b : M) (c : R) :
@[protected, instance]
Equations

For any given denominator b : M, the map a ↦ a / b is an add_monoid_hom from R to localization M

Equations
theorem localization.mk_sum {R : Type u_1} [comm_semiring R] {M : submonoid R} {ι : Type u_2} (f : ι R) (s : finset ι) (b : M) :
localization.mk (s.sum (λ (i : ι), f i)) b = s.sum (λ (i : ι), localization.mk (f i) b)
theorem localization.mk_list_sum {R : Type u_1} [comm_semiring R] {M : submonoid R} (l : list R) (b : M) :
localization.mk l.sum b = (list.map (λ (a : R), localization.mk a b) l).sum
theorem localization.mk_multiset_sum {R : Type u_1} [comm_semiring R] {M : submonoid R} (l : multiset R) (b : M) :
@[protected, instance]
def localization.algebra {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra S R] :
Equations
@[protected, instance]
theorem localization.mk_algebra_map {R : Type u_1} [comm_semiring R] {M : submonoid R} {A : Type u_2} [comm_semiring A] [algebra A R] (m : A) :
theorem localization.mk_nat_cast {R : Type u_1} [comm_semiring R] {M : submonoid R} (m : ) :
noncomputable def localization.alg_equiv {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring 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
noncomputable def is_localization.unique (R : Type u_1) (Rₘ : Type u_2) [comm_semiring R] [comm_semiring Rₘ] (M : submonoid R) [subsingleton R] [algebra R Rₘ] [is_localization M Rₘ] :
unique Rₘ

The localization of a singleton is a singleton. Cannot be an instance due to metavariables.

Equations
@[simp]
theorem localization.alg_equiv_mk {R : Type u_1} [comm_semiring R] {M : submonoid R} {S : Type u_2} [comm_semiring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[protected, irreducible]
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]
Equations
theorem localization.neg_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (a : R) (b : M) :
@[protected, instance]
Equations
theorem localization.sub_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (a c : R) (b d : M) :
theorem localization.mk_int_cast {R : Type u_1} [comm_ring R] {M : submonoid R} (m : ) :
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 non_zero_divisors R) :
(algebra_map R S) x = 0 x = 0
@[protected]
@[protected]
theorem is_localization.sec_snd_ne_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] [nontrivial R] (hM : M non_zero_divisors R) (x : S) :
theorem is_localization.sec_fst_ne_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] [nontrivial R] [no_zero_divisors S] (hM : M non_zero_divisors R) {x : S} (hx : x 0) :

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

@[reducible]

A comm_ring S which is the localization of a ring R without zero divisors at a subset of non-zero elements does not have zero divisors. See note [reducible non-instances].

@[reducible]

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

@[reducible]

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

theorem is_field.localization_map_bijective {R : Type u_1} {Rₘ : Type u_2} [comm_ring 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.

theorem field.localization_map_bijective {K : Type u_1} {Kₘ : Type u_2} [field K] [comm_ring Kₘ] {M : submonoid K} (hM : 0 M) [algebra K Kₘ] [is_localization M Kₘ] :

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

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_4} {Sₘ : Type u_5} [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.

This instance can be helpful if you define Sₘ := localization (algebra.algebra_map_submonoid S M), however we will instead use the hypotheses [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] in lemmas since the algebra structure may arise in different ways.

Equations
theorem is_localization.map_units_map_submonoid {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] (Sₘ : Type u_5) [comm_ring Sₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] [algebra R Sₘ] [is_scalar_tower R S Sₘ] (y : M) :
@[simp]
theorem is_localization.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_4) (Sₘ : Type u_5) [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ₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] (x : R) (y : M) :
theorem is_localization.algebra_map_eq_map_map_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [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ₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] :

If the square below commutes, the bottom map is uniquely specified:

R    S
     
Rₘ  Sₘ
theorem is_localization.algebra_map_apply_eq_map_map_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [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ₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] (x : Rₘ) :
(algebra_map Rₘ Sₘ) x = (is_localization.map Sₘ (algebra_map R S) _) x

If the square below commutes, the bottom map is uniquely specified:

R    S
     
Rₘ  Sₘ
theorem is_localization.lift_algebra_map_eq_algebra_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [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ₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] :
theorem localization_algebra_injective {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [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ₘ] (hRS : function.injective (algebra_map R S)) :

Injectivity of the underlying algebra_map descends to the algebra induced by localization.