mathlib3documentation

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 #

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

Main results #

• `localization M S`, a construction of the localization as a quotient type, defined in `group_theory.monoid_localization`, has `comm_ring`, `algebra R` and `is_localization M` instances if `R` is a ring. `localization.away`, `localization.at_prime` and `fraction_ring` are abbreviations for `localization`s and have their corresponding `is_localization` instances

Implementation notes #

In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally `rewrite` one structure with an isomorphic one; one way around this is to isolate a predicate characterizing a structure up to isomorphism, and reason about things that satisfy the predicate.

A previous version of this file used a fully bundled type of ring localization maps, then used a type synonym `f.codomain` for `f : localization_map M S` to instantiate the `R`-algebra structure on `S`. This results in defining ad-hoc copies for everything already defined on `S`. By making `is_localization` a predicate on the `algebra_map R S`, we can ensure the localization map commutes nicely with other `algebra_map`s.

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} (M : submonoid R) (S : Type u_2) [ 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} (M : submonoid R) {S : Type u_2} [ S] [ S] (N : submonoid R) (h₁ : M N) (h₂ : (r : R), r N is_unit ( S) r)) :
def is_localization.to_localization_with_zero_map {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :

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

Equations
@[simp]
@[reducible]
def is_localization.to_localization_map {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :

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

@[simp]
theorem is_localization.to_localization_map_to_map {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :
theorem is_localization.to_localization_map_to_map_apply {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (x : R) :
= S) x
noncomputable def is_localization.sec {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] [ 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
@[simp]
theorem is_localization.to_localization_map_sec {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] [ S] :
theorem is_localization.sec_spec {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] [ S] (z : S) :
z * S) z).snd) = S) z).fst

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} (M : submonoid R) {S : Type u_2} [ S] [ S] (z : S) :
S) z).fst = S) z).snd) * z

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} {M : submonoid R} {S : Type u_2} [ S] [ S] {x y : R} {c : M} (h : S) (c * x) = S) (c * y)) :
S) x = S) y
theorem is_localization.map_left_cancel {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] {x y : R} {c : M} (h : S) (x * c) = S) (y * c)) :
S) x = S) y
theorem is_localization.eq_zero_of_fst_eq_zero {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] {z : S} {x : R} {y : M} (h : z * S) y = S) x) (hx : x = 0) :
z = 0
theorem is_localization.map_eq_zero_iff {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (r : R) :
S) r = 0 (m : M), m * r = 0
noncomputable def is_localization.mk' {R : Type u_1} {M : submonoid R} (S : Type u_2) [ S] [ S] (x : R) (y : M) :
S

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

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

Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `comm_semiring`s `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} {M : submonoid R} {S : Type u_2} [ S] [ S] (x₁ x₂ : R) (y₁ y₂ : M) :
(x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = y₁ + y₂
theorem is_localization.mul_add_inv_left {R : Type u_1} {M : submonoid R} {P : Type u_3} {g : R →+* P} (h : (y : M), is_unit (g y)) (y : M) (w z₁ z₂ : P) :
w * ( h) y)⁻¹ + z₁ = z₂ w + g y * z₁ = g y * z₂
theorem is_localization.lift_spec_mul_add {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) (z : S) (w w' v : P) :
+ w' = v g z).fst * w + g z).snd) * w' = g z).snd) * v
noncomputable def is_localization.lift {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ 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_semiring`s `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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) (x : R) (y : M) :
y) = g x * ( hg) y)⁻¹

Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `comm_semiring`s `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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) (x : R) (v : P) (y : M) :
y) = v g x = g y * v
@[simp]
theorem is_localization.lift_eq {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) (x : R) :
( S) x) = g x
theorem is_localization.lift_eq_iff {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) {x y : R × M} :
x.snd) = y.snd) g (x.fst * (y.snd)) = g (y.fst * (x.snd))
@[simp]
theorem is_localization.lift_comp {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) :
.comp S) = g
@[simp]
theorem is_localization.lift_of_comp {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] (j : S →+* P) :
theorem is_localization.monoid_hom_ext {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ S] ⦃j k : S →* P⦄ (h : j.comp S) = k.comp S)) :
j = k
theorem is_localization.ring_hom_ext {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ S] ⦃j k : S →+* P⦄ (h : j.comp S) = k.comp S)) :
j = k
theorem is_localization.alg_hom_subsingleton {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ S] [ P] :
@[protected]
theorem is_localization.ext {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ 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 ( S) a) = k ( 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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) {j : S →+* P} (hj : (x : R), j ( S) x) = g x) :
@[simp]
theorem is_localization.lift_id {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] (x : S) :
= x
theorem is_localization.lift_surjective_iff {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) :
(v : P), (x : R × M), v * g (x.snd) = g x.fst
theorem is_localization.lift_injective_iff {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} (hg : (y : M), is_unit (g y)) :
(x y : R), S) x = S) y g x = g y
noncomputable def is_localization.map {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {T : submonoid P} (Q : Type u_4) [ Q] [ Q] (g : R →+* P) (hy : M ) :
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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] (x : R) :
hy) ( S) x) = Q) (g x)
@[simp]
theorem is_localization.map_comp {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] :
hy).comp S) = Q).comp g
theorem is_localization.map_mk' {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] (x : R) (y : M) :
hy) y) = (g x) g y, _⟩
@[simp]
theorem is_localization.map_id {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] (z : S) (h : M := _) :
h) z = z
theorem is_localization.map_unique {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] (j : S →+* Q) (hj : (x : R), j ( S) x) = Q) (g x)) :
hy = j
theorem is_localization.map_comp_map {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] {A : Type u_5} {U : submonoid A} {W : Type u_6} [ W] [ W] {l : P →+* A} (hl : T ) :
hl).comp hy) = (l.comp g) _

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

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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} (hy : M ) [ Q] [ Q] (x : S) (z : R) :
hy) (z x) = g z hy) x
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_apply {R : Type u_1} {M : submonoid R} (S : Type u_2) [ S] {P : Type u_3} [ S] {T : submonoid P} (Q : Type u_4) [ Q] [ Q] (h : R ≃+* P) (H : = T) (ᾰ : S) :
= _)
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_symm_apply {R : Type u_1} {M : submonoid R} (S : Type u_2) [ S] {P : Type u_3} [ S] {T : submonoid P} (Q : Type u_4) [ Q] [ Q] (h : R ≃+* P) (H : = T) (ᾰ : Q) :
H).symm) = (h.symm) _)
noncomputable def is_localization.ring_equiv_of_ring_equiv {R : Type u_1} {M : submonoid R} (S : Type u_2) [ S] {P : Type u_3} [ S] {T : submonoid P} (Q : Type u_4) [ Q] [ Q] (h : R ≃+* P) (H : = 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} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {T : submonoid P} {Q : Type u_4} [ Q] [ Q] {j : R ≃+* P} (H : = T) :
= _
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_eq {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {T : submonoid P} {Q : Type u_4} [ Q] [ Q] {j : R ≃+* P} (H : = T) (x : R) :
( S) x) = Q) (j x)
theorem is_localization.ring_equiv_of_ring_equiv_mk' {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] {P : Type u_3} [ S] {T : submonoid P} {Q : Type u_4} [ Q] [ Q] {j : R ≃+* P} (H : = T) (x : R) (y : M) :
y) = (j x) j y, _⟩
noncomputable def is_localization.alg_equiv {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (Q : Type u_4) [ Q] [ 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} (M : submonoid R) (S : Type u_2) [ S] [ S] (Q : Type u_4) [ Q] [ Q] (ᾰ : S) :
Q) =
@[simp]
theorem is_localization.alg_equiv_symm_apply {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (Q : Type u_4) [ Q] [ Q] (ᾰ : Q) :
Q).symm) =
@[simp]
theorem is_localization.alg_equiv_mk' {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] {Q : Type u_4} [ Q] [ Q] (x : R) (y : M) :
Q) y) = y
@[simp]
theorem is_localization.alg_equiv_symm_mk' {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] {Q : Type u_4} [ Q] [ Q] (x : R) (y : M) :
Q).symm) y) = y
theorem is_localization.is_localization_of_alg_equiv {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ P] [ S] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_alg_equiv {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} [ P] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_ring_equiv {R : Type u_1} (M : submonoid R) {S : Type u_2} [ S] {P : Type u_3} (h : S ≃+* P) :
theorem is_localization.is_localization_of_base_ring_equiv {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] {P : Type u_3} [ S] (h : R ≃+* P) :
theorem is_localization.is_localization_iff_of_base_ring_equiv {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] {P : Type u_3} (h : R ≃+* P) :
theorem is_localization.non_zero_divisors_le_comap {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :
theorem is_localization.map_non_zero_divisors_le {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :

Constructing a localization at a given submonoid #

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

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} {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} {M : submonoid R} (l : list R) (b : M) :
= (list.map (λ (a : R), b) l).sum
theorem localization.mk_multiset_sum {R : Type u_1} {M : submonoid R} (l : multiset R) (b : M) :
= (multiset.map (λ (a : R), b) l).sum
@[protected, instance]
def localization.distrib_mul_action {R : Type u_1} {M : submonoid R} {S : Type u_2} [monoid S] [ R] [ R] :
Equations
@[protected, instance]
def localization.mul_semiring_action {R : Type u_1} {M : submonoid R} {S : Type u_2} [semiring S] [ R] [ R] :
Equations
@[protected, instance]
def localization.module {R : Type u_1} {M : submonoid R} {S : Type u_2} [semiring S] [ R] [ R] :
Equations
@[protected, instance]
def localization.algebra {R : Type u_1} {M : submonoid R} {S : Type u_2} [ R] :
Equations
@[protected, instance]
def localization.is_localization {R : Type u_1} {M : submonoid R} :
theorem localization.monoid_of_eq_algebra_map {R : Type u_1} {M : submonoid R} (x : R) :
x = (localization M)) x
theorem localization.mk_one_eq_algebra_map {R : Type u_1} {M : submonoid R} (x : R) :
theorem localization.mk_eq_mk'_apply {R : Type u_1} {M : submonoid R} (x : R) (y : M) :
= y
@[simp]
theorem localization.mk_eq_mk' {R : Type u_1} {M : submonoid R} :
theorem localization.mk_algebra_map {R : Type u_1} {M : submonoid R} {A : Type u_2} [ R] (m : A) :
theorem localization.mk_nat_cast {R : Type u_1} {M : submonoid R} (m : ) :
= m
noncomputable def localization.alg_equiv {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ 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} (M : submonoid R) (S : Type u_2) [ S] [ S] (ᾰ : S) :
S).symm) = ((ring_equiv.refl R).symm) _)
@[simp]
theorem localization.alg_equiv_apply {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (ᾰ : localization M) :
= _)
noncomputable def is_localization.unique (R : Type u_1) (Rₘ : Type u_2) [comm_semiring Rₘ] (M : submonoid R) [subsingleton R] [ Rₘ] [ 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} {M : submonoid R} {S : Type u_2} [ S] [ S] (x : R) (y : M) :
y) = y
@[simp]
theorem localization.alg_equiv_symm_mk' {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] (x : R) (y : M) :
S).symm) y) = y
theorem localization.alg_equiv_mk {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] (x : R) (y : M) :
y) = y
theorem localization.alg_equiv_symm_mk {R : Type u_1} {M : submonoid R} {S : Type u_2} [ S] [ S] (x : R) (y : M) :
S).symm) y) =
@[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
• z.neg = z.lift_on (λ (a : R) (b : M), b) localization.neg._proof_1
@[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) :
- = b
@[protected, instance]
def localization.comm_ring {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
theorem localization.sub_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (a c : R) (b d : M) :
- = localization.mk (d * a - b * c) (b * d)
theorem localization.mk_int_cast {R : Type u_1} [comm_ring R] {M : submonoid R} (m : ) :
= 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] [ S] [ S] {x : R} (hM : M ) :
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] [ S] [ S] (hM : M ) :
@[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] [ S] [ S] [nontrivial R] (hM : M ) {x : R} (hx : x ) :
S) x 0
theorem is_localization.sec_snd_ne_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] [nontrivial R] (hM : M ) (x : S) :
x).snd) 0
theorem is_localization.sec_fst_ne_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] [nontrivial R] (hM : M ) {x : S} (hx : x 0) :
x).fst 0
theorem is_localization.map_injective_of_injective {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] (Q : Type u_5) [comm_ring Q] {g : R →+* P} [ Q] (hg : function.injective g) [ Q] :

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

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

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]
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] [ S] {M : submonoid A} [ S] (hM : M ) :

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]
theorem is_localization.is_domain_localization {A : Type u_6} [comm_ring A] [is_domain A] {M : submonoid A} (hM : M ) :

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) [ Rₘ] [ 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) [ Kₘ] [ 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] [ S] {Rₘ : Type u_4} {Sₘ : Type u_5} [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ 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] [ S] (Sₘ : Type u_5) [comm_ring Sₘ] [ Sₘ] [ Sₘ] [ Sₘ] [ Sₘ] (y : M) :
is_unit ( Sₘ) y)
@[simp]
theorem is_localization.algebra_map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] (Rₘ : Type u_4) (Sₘ : Type u_5) [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] [algebra Rₘ Sₘ] [ Sₘ] [ Rₘ Sₘ] [ Sₘ] (x : R) (y : M) :
(algebra_map Rₘ Sₘ) x y) = ( S) x) S) y, _⟩
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] [ S] (Rₘ : Type u_4) (Sₘ : Type u_5) [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] [algebra Rₘ Sₘ] [ Sₘ] [ Rₘ Sₘ] [ Sₘ] :
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] [ S] (Rₘ : Type u_4) (Sₘ : Type u_5) [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] [algebra Rₘ Sₘ] [ Sₘ] [ Rₘ Sₘ] [ Sₘ] (x : Rₘ) :
(algebra_map Rₘ Sₘ) x = 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] [ S] (Rₘ : Type u_4) (Sₘ : Type u_5) [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] [algebra Rₘ Sₘ] [ Sₘ] [ Rₘ Sₘ] [ Sₘ] :
= Sₘ
theorem localization_algebra_injective {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] (Rₘ : Type u_4) (Sₘ : Type u_5) [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] (hRS : function.injective S)) :

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