# Localizations of commutative rings #

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

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

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

variable (R S P Q : Type*) [CommRing R] [CommRing S] [CommRing P] [CommRing Q]
variable [Algebra R S] [Algebra P Q] (M : Submonoid R) (T : Submonoid P)


## Main definitions #

• IsLocalization (M : Submonoid R) (S : Type*) is a typeclass expressing that S is a localization of R at M, i.e. the canonical map algebraMap R S : R →+* S is a localization map (satisfying the above properties).
• IsLocalization.mk' S is a surjection sending (x, y) : R × M to f x * (f y)⁻¹
• IsLocalization.lift is the ring homomorphism from S induced by a homomorphism from R which maps elements of M to invertible elements of the codomain.
• IsLocalization.map S Q is the ring homomorphism from S to Q which maps elements of M to elements of T
• IsLocalization.ringEquivOfRingEquiv: if R and P are isomorphic by an isomorphism sending M to T, then S and Q are isomorphic
• IsLocalization.algEquiv: 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 GroupTheory.MonoidLocalization, has CommRing, Algebra R and IsLocalization M instances if R is a ring. Localization.Away, Localization.AtPrime and FractionRing are abbreviations for Localizations and have their corresponding IsLocalization 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 : LocalizationMap M S to instantiate the R-algebra structure on S. This results in defining ad-hoc copies for everything already defined on S. By making IsLocalization a predicate on the algebraMap R S, we can ensure the localization map commutes nicely with other algebraMaps.

To prove most lemmas about a localization map algebraMap R S in this file we invoke the corresponding proof for the underlying CommMonoid localization map IsLocalization.toLocalizationMap M S, which can be found in GroupTheory.MonoidLocalization and the namespace Submonoid.LocalizationMap.

To reason about the localization as a quotient type, use mk_eq_of_mk' and associated lemmas. These show the quotient map mk : R → M → Localization M equals the surjection LocalizationMap.mk' induced by the map algebraMap : R →+* Localization M. The lemma mk_eq_of_mk' hence gives you access to the results in the rest of the file, which are about the LocalizationMap.mk' induced by any localization map.

The proof that "a CommRing K which is the localization of an integral domain R at R \ {0} is a field" is a def rather than an instance, so if you want to reason about a field of fractions K, assume [Field K] instead of just [CommRing K].

## Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

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

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

• map_units' : ∀ (y : M), IsUnit (() y)

Everything in the image of algebraMap is a unit

• surj' : ∀ (z : S), ∃ (x : R × M), z * () x.2 = () x.1

The algebraMap is surjective

• exists_of_eq : ∀ {x y : R}, () x = () y∃ (c : M), c * x = c * y

The kernel of algebraMap is contained in the annihilator of M; it is then equal to the annihilator by map_units'

Instances
theorem IsLocalization.map_units' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [self : ] (y : M) :
IsUnit (() y)

Everything in the image of algebraMap is a unit

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

The algebraMap is surjective

theorem IsLocalization.exists_of_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [self : ] {x : R} {y : R} :
() x = () y∃ (c : M), c * x = c * y

The kernel of algebraMap is contained in the annihilator of M; it is then equal to the annihilator by map_units'

theorem IsLocalization.map_units {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (y : M) :
IsUnit (() y)

Everything in the image of algebraMap is a unit

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

The algebraMap is surjective

theorem IsLocalization.eq_iff_exists {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] {x : R} {y : R} :
() x = () y ∃ (c : M), c * x = c * y

The kernel of algebraMap is contained in the annihilator of M; it is then equal to the annihilator by map_units'

theorem IsLocalization.of_le {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (N : ) (h₁ : M N) (h₂ : rN, IsUnit (() r)) :
@[simp]
theorem IsLocalization.toLocalizationWithZeroMap_toFun {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (a : R) :
(.toMonoidHom).toFun a = () a
def IsLocalization.toLocalizationWithZeroMap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
M.LocalizationWithZeroMap S

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev IsLocalization.toLocalizationMap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
M.LocalizationMap S

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

Equations
• = .toLocalizationMap
Instances For
@[simp]
theorem IsLocalization.toLocalizationMap_toMap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
.toMap = ()
theorem IsLocalization.toLocalizationMap_toMap_apply {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (x : R) :
.toMap x = () x
theorem IsLocalization.surj₂ {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (z : S) (w : S) :
∃ (z' : R) (w' : R) (d : M), z * () d = () z' w * () d = () w'
noncomputable def IsLocalization.sec {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R 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
Instances For
@[simp]
theorem IsLocalization.toLocalizationMap_sec {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] :
theorem IsLocalization.sec_spec {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (z : S) :
z * () ().2 = () ().1

Given z : S, IsLocalization.sec M z is defined to be a pair (x, y) : R × M such that z * f y = f x (so this lemma is true by definition).

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

Given z : S, IsLocalization.sec M z is defined to be a pair (x, y) : R × M such that z * f y = f x, so this lemma is just an application of S's commutativity.

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

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

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

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

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

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

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

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

Equations
Instances For
theorem IsLocalization.mk'_eq_iff_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {x₁ : R} {x₂ : R} {y₁ : M} {y₂ : M} :
IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ () (y₂ * x₁) = () (y₁ * x₂)
theorem IsLocalization.mk'_eq_iff_eq' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {x₁ : R} {x₂ : R} {y₁ : M} {y₂ : M} :
IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ () (x₁ * y₂) = () (x₂ * y₁)
theorem IsLocalization.mk'_mem_iff {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {x : R} {y : M} {I : } :
I () x I
theorem IsLocalization.eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {a₁ : R} {b₁ : R} {a₂ : M} {b₂ : M} :
IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂ ∃ (c : M), c * (b₂ * a₁) = c * (a₂ * b₁)
theorem IsLocalization.mk'_eq_zero_iff {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (s : M) :
= 0 ∃ (m : M), m * x = 0
@[simp]
theorem IsLocalization.mk'_zero {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (s : M) :
= 0
theorem IsLocalization.ne_zero_of_mk'_ne_zero {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {x : R} {y : M} (hxy : 0) :
x 0
theorem IsLocalization.eq_iff_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] [Algebra R P] [] {x : R} {y : R} :
() x = () y () x = () y
theorem IsLocalization.mk'_eq_iff_mk'_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] [Algebra R P] [] {x₁ : R} {x₂ : R} {y₁ : M} {y₂ : M} :
IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ IsLocalization.mk' P x₁ y₁ = IsLocalization.mk' P x₂ y₂
theorem IsLocalization.mk'_eq_of_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {a₁ : R} {b₁ : R} {a₂ : M} {b₂ : M} (H : a₂ * b₁ = b₂ * a₁) :
IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
theorem IsLocalization.mk'_eq_of_eq' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {a₁ : R} {b₁ : R} {a₂ : M} {b₂ : M} (H : b₁ * a₂ = a₁ * b₂) :
IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
theorem IsLocalization.mk'_cancel {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (a : R) (b : M) (c : M) :
IsLocalization.mk' S (a * c) (b * c) =
@[simp]
theorem IsLocalization.mk'_self {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] {x : R} (hx : x M) :
IsLocalization.mk' S x x, hx = 1
@[simp]
theorem IsLocalization.mk'_self' {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] {x : M} :
IsLocalization.mk' S (x) x = 1
theorem IsLocalization.mk'_self'' {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] {x : M} :
IsLocalization.mk' S (x) x = 1
theorem IsLocalization.mul_mk'_eq_mk'_of_mul {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : R) (z : M) :
() x * = IsLocalization.mk' S (x * y) z
theorem IsLocalization.mk'_eq_mul_mk'_one {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : M) :
= () x *
@[simp]
theorem IsLocalization.mk'_mul_cancel_left {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : M) :
IsLocalization.mk' S (y * x) y = () x
theorem IsLocalization.mk'_mul_cancel_right {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : M) :
IsLocalization.mk' S (x * y) y = () x
@[simp]
theorem IsLocalization.mk'_mul_mk'_eq_one {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : M) (y : M) :
IsLocalization.mk' S (x) y * IsLocalization.mk' S (y) x = 1
theorem IsLocalization.mk'_mul_mk'_eq_one' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : M) (h : x M) :
* IsLocalization.mk' S y x, h = 1
theorem IsLocalization.smul_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (y : R) (m : M) :
@[simp]
theorem IsLocalization.smul_mk'_one {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : R) (m : M) :
x =
@[simp]
theorem IsLocalization.smul_mk'_self {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {m : M} {r : R} :
m = () r
@[simp]
theorem IsLocalization.invertible_mk'_one_invOf {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (s : M) :
() = () s
instance IsLocalization.invertible_mk'_one {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (s : M) :
Equations
• = { invOf := () s, invOf_mul_self := , mul_invOf_self := }
theorem IsLocalization.isUnit_comp {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] (j : S →+* P) (y : M) :
IsUnit ((j.comp ()) y)
theorem IsLocalization.eq_of_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) {x : R} {y : R} (h : () x = () y) :
g x = g y

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

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

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g y is invertible for all y : M, the homomorphism induced from S to P sending z : S to g x * (g y)⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsLocalization.lift_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) (x : R) (y : M) :
() () = g x * ((IsUnit.liftRight ((g).restrict M) hg) y)⁻¹

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →* P such that g y is invertible for all y : M, the homomorphism induced from S to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : R, y ∈ M.

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

See note [partially-applied ext lemmas]

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

See note [partially-applied ext lemmas]

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

To show j and k agree on the whole localization, it suffices to show they agree on the image of the base ring, if they preserve 1 and *.

theorem IsLocalization.lift_unique {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) {j : S →+* P} (hj : ∀ (x : R), j (() x) = g x) :
@[simp]
theorem IsLocalization.lift_id {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (x : S) :
x = x
theorem IsLocalization.lift_surjective_iff {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
∀ (v : P), ∃ (x : R × M), v * g x.2 = g x.1
theorem IsLocalization.lift_injective_iff {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (hg : ∀ (y : M), IsUnit (g y)) :
∀ (x y : R), () x = () y g x = g y
noncomputable def IsLocalization.map {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {T : } (Q : Type u_4) [] [Algebra P 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 algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations
Instances For
@[simp]
theorem IsLocalization.map_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] (x : R) :
() (() x) = () (g x)
@[simp]
theorem IsLocalization.map_comp {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] :
().comp () = ().comp g
theorem IsLocalization.map_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] (x : R) (y : M) :
() () = IsLocalization.mk' Q (g x) g y,
@[simp]
theorem IsLocalization.map_id_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {Q : Type u_5} [] [Algebra R Q] [] (x : R) (y : M) :
() () =
@[simp]
theorem IsLocalization.map_id {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (z : S) (h : optParam (M ) ) :
() z = z
theorem IsLocalization.map_unique {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] (j : S →+* Q) (hj : ∀ (x : R), j (() x) = () (g x)) :
= j
theorem IsLocalization.map_comp_map {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] {A : Type u_5} [] {U : } {W : Type u_6} [] [Algebra A W] [] {l : P →+* A} (hl : T ) :
().comp () = IsLocalization.map W (l.comp g)

If CommSemiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

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

If CommSemiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

theorem IsLocalization.map_smul {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} {T : } {Q : Type u_4} [] (hy : M ) [Algebra P Q] [] (x : S) (z : R) :
() (z x) = g z () x
@[simp]
theorem IsLocalization.ringEquivOfRingEquiv_symm_apply {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] [] {T : } (Q : Type u_4) [] [Algebra P Q] [] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : Q) :
().symm a = (IsLocalization.map S h.symm ) a
@[simp]
theorem IsLocalization.ringEquivOfRingEquiv_apply {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] [] {T : } (Q : Type u_4) [] [Algebra P Q] [] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : S) :
() a = () a
noncomputable def IsLocalization.ringEquivOfRingEquiv {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] [] {T : } (Q : Type u_4) [] [Algebra P Q] [] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) :
S ≃+* Q

If S, Q are localizations of R and P at submonoids M, T respectively, an isomorphism j : R ≃+* P such that j(M) = T induces an isomorphism of localizations S ≃+* Q.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsLocalization.ringEquivOfRingEquiv_eq_map {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {T : } {Q : Type u_4} [] [Algebra P Q] [] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) :
() =
theorem IsLocalization.ringEquivOfRingEquiv_eq {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {T : } {Q : Type u_4} [] [Algebra P Q] [] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) :
() (() x) = () (j x)
theorem IsLocalization.ringEquivOfRingEquiv_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [] {T : } {Q : Type u_4} [] [Algebra P Q] [] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) (y : M) :
() () = IsLocalization.mk' Q (j x) j y,
@[simp]
theorem IsLocalization.algEquiv_apply {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (Q : Type u_4) [] [Algebra R Q] [] (a : S) :
() a = () a
@[simp]
theorem IsLocalization.algEquiv_symm_apply {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (Q : Type u_4) [] [Algebra R Q] [] (a : Q) :
().symm a = () a
noncomputable def IsLocalization.algEquiv {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (Q : Type u_4) [] [Algebra R Q] [] :

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

Equations
• = let __src := ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
theorem IsLocalization.algEquiv_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {Q : Type u_4} [] [Algebra R Q] [] (x : R) (y : M) :
() () =
theorem IsLocalization.algEquiv_symm_mk' {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] {Q : Type u_4} [] [Algebra R Q] [] (x : R) (y : M) :
().symm () =
theorem IsLocalization.at_units {R : Type u_4} [] (S : ) (hS : ) :
noncomputable def IsLocalization.atUnits (R : Type u_1) [] (M : ) {S : Type u_2} [] [Algebra R S] [] (H : ) :

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

Equations
Instances For
theorem IsLocalization.map_injective_of_injective {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] [] {g : R →+* P} (Q : Type u_4) [] [Algebra P Q] (h : ) [IsLocalization () Q] :

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

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

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

theorem IsLocalization.isLocalization_of_algEquiv {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [Algebra R P] [] (h : S ≃ₐ[R] P) :
theorem IsLocalization.isLocalization_iff_of_algEquiv {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] [Algebra R P] (h : S ≃ₐ[R] P) :
theorem IsLocalization.isLocalization_iff_of_ringEquiv {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] (h : S ≃+* P) :
theorem IsLocalization.isLocalization_of_base_ringEquiv {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] [] (h : R ≃+* P) :
IsLocalization (Submonoid.map h.toMonoidHom M) S
theorem IsLocalization.isLocalization_iff_of_base_ringEquiv {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] (h : R ≃+* P) :
IsLocalization (Submonoid.map h.toMonoidHom M) S
theorem IsLocalization.nonZeroDivisors_le_comap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
theorem IsLocalization.map_nonZeroDivisors_le {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :

### Constructing a localization at a given submonoid #

instance Localization.instUniqueLocalization {R : Type u_1} [] {M : } [] :
Equations
• Localization.instUniqueLocalization = { toInhabited := OreLocalization.instInhabited, uniq := }
theorem Localization.add_mk {R : Type u_1} [] {M : } (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 : } (a : R) (b : M) (c : R) :
+ = Localization.mk (a + c) b
@[simp]
theorem Localization.mkAddMonoidHom_apply {R : Type u_1} [] {M : } (b : M) (a : R) :
def Localization.mkAddMonoidHom {R : Type u_1} [] {M : } (b : M) :

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

Equations
• = { toFun := fun (a : R) => , map_zero' := , map_add' := }
Instances For
theorem Localization.mk_sum {R : Type u_1} [] {M : } {ι : Type u_4} (f : ιR) (s : ) (b : M) :
Localization.mk (is, f i) b = is, Localization.mk (f i) b
theorem Localization.mk_list_sum {R : Type u_1} [] {M : } (l : List R) (b : M) :
Localization.mk l.sum b = (List.map (fun (a : R) => ) l).sum
theorem Localization.mk_multiset_sum {R : Type u_1} [] {M : } (l : ) (b : M) :
Localization.mk l.sum b = (Multiset.map (fun (a : R) => ) l).sum
instance Localization.isLocalization {R : Type u_1} [] {M : } :
Equations
• =
@[simp]
theorem Localization.toLocalizationMap_eq_monoidOf {R : Type u_1} [] {M : } :
theorem Localization.monoidOf_eq_algebraMap {R : Type u_1} [] {M : } (x : R) :
.toMap x = () x
theorem Localization.mk_one_eq_algebraMap {R : Type u_1} [] {M : } (x : R) :
= () x
theorem Localization.mk_eq_mk'_apply {R : Type u_1} [] {M : } (x : R) (y : M) :
=
theorem Localization.mk_eq_mk' {R : Type u_1} [] {M : } :
Localization.mk =
theorem Localization.mk_algebraMap {R : Type u_1} [] {M : } {A : Type u_4} [] [Algebra A R] (m : A) :
Localization.mk (() m) 1 = () m
theorem Localization.mk_natCast {R : Type u_1} [] {M : } (m : ) :
Localization.mk (m) 1 = m
@[deprecated Localization.mk_natCast]
theorem Localization.mk_nat_cast {R : Type u_1} [] {M : } (m : ) :
Localization.mk (m) 1 = m

Alias of Localization.mk_natCast.

@[simp]
theorem Localization.algEquiv_symm_apply {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (a : S) :
().symm a = () a
@[simp]
theorem Localization.algEquiv_apply {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (a : ) :
() a = () a
noncomputable def Localization.algEquiv {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :

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

Equations
Instances For
noncomputable def IsLocalization.unique (R : Type u_4) (Rₘ : Type u_5) [] [] (M : ) [] [Algebra R Rₘ] [] :
Unique Rₘ

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

Equations
• = let_fun this := { default := 1 }; .unique
Instances For
theorem Localization.algEquiv_mk' {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (x : R) (y : M) :
() () =
theorem Localization.algEquiv_symm_mk' {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (x : R) (y : M) :
().symm () =
theorem Localization.algEquiv_mk {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (x : R) (y : M) :
() () =
theorem Localization.algEquiv_symm_mk {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (x : R) (y : M) :
().symm () =
theorem Localization.coe_algEquiv {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] :
() =
theorem Localization.coe_algEquiv_symm {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] :
().symm =
theorem Localization.neg_mk {R : Type u_1} [] {M : } (a : R) (b : M) :
theorem Localization.sub_mk {R : Type u_1} [] {M : } (a : R) (c : R) (b : M) (d : M) :
- = Localization.mk (d * a - b * c) (b * d)
theorem Localization.mk_intCast {R : Type u_1} [] {M : } (m : ) :
Localization.mk (m) 1 = m
@[deprecated Localization.mk_intCast]
theorem Localization.mk_int_cast {R : Type u_1} [] {M : } (m : ) :
Localization.mk (m) 1 = m

Alias of Localization.mk_intCast.

theorem IsLocalization.to_map_eq_zero_iff {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] {x : R} (hM : ) :
() x = 0 x = 0
theorem IsLocalization.injective {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (hM : ) :
theorem IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] [] (hM : ) {x : R} (hx : ) :
() x 0
theorem IsLocalization.sec_snd_ne_zero {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] [] (hM : ) (x : S) :
().2 0
theorem IsLocalization.sec_fst_ne_zero {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] [] [] (hM : ) {x : S} (hx : x 0) :
().1 0
theorem IsLocalization.noZeroDivisors_of_le_nonZeroDivisors {S : Type u_2} [] (A : Type u_6) [] [] [Algebra A S] {M : } [] (hM : ) :

A CommRing S which is the localization of a ring R without zero divisors at a subset of non-zero elements does not have zero divisors.

theorem IsLocalization.isDomain_of_le_nonZeroDivisors {S : Type u_2} [] (A : Type u_6) [] [] [Algebra A S] {M : } [] (hM : ) :

A CommRing S which is the localization of an integral domain R at a subset of non-zero elements is an integral domain.

theorem IsLocalization.isDomain_localization {A : Type u_6} [] [] {M : } (hM : ) :

The localization of an integral domain to a set of non-zero elements is an integral domain.

theorem IsField.localization_map_bijective {R : Type u_4} {Rₘ : Type u_5} [] [CommRing Rₘ] {M : } (hM : 0M) (hR : ) [Algebra 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_4} {Kₘ : Type u_5} [] [CommRing Kₘ] {M : } (hM : 0M) [Algebra K Kₘ] [] :

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

noncomputable def localizationAlgebra {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] :
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 algebraMap 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.algebraMapSubmonoid S M), however we will instead use the hypotheses [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] in lemmas since the algebra structure may arise in different ways.

Equations
Instances For
theorem IsLocalization.map_units_map_submonoid {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [i : ] [Algebra R Sₘ] [IsScalarTower R S Sₘ] (y : M) :
IsUnit ((algebraMap R Sₘ) y)
theorem IsLocalization.algebraMap_mk' {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : R) (y : M) :
(algebraMap Rₘ Sₘ) () = IsLocalization.mk' Sₘ (() x) () y,
theorem IsLocalization.algebraMap_eq_map_map_submonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] :
algebraMap Rₘ Sₘ = IsLocalization.map Sₘ ()

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

R  →  S
↓     ↓
Rₘ → Sₘ

theorem IsLocalization.algebraMap_apply_eq_map_map_submonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : Rₘ) :
(algebraMap Rₘ Sₘ) x = (IsLocalization.map Sₘ () ) x

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

R  →  S
↓     ↓
Rₘ → Sₘ

theorem IsLocalization.lift_algebraMap_eq_algebraMap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] :
= algebraMap Rₘ Sₘ
theorem localizationAlgebra_injective {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [i : ] (hRS : Function.Injective ()) :

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