mathlib documentation

ring_theory.localization

Localizations of commutative rings #

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

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

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

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

Main definitions #

Main results #

Implementation notes #

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

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

To prove most lemmas about a localization map algebra_map R S in this file we invoke the corresponding proof for the underlying comm_monoid localization map is_localization.to_localization_map M S, which can be found in group_theory.monoid_localization and the namespace submonoid.localization_map.

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

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

Tags #

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

@[class]
structure is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring 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
def is_localization.to_localization_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

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

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

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

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

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the right, matching the argument order in localization_map.surj.

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

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the left, matching the argument order in the has_scalar instance.

def is_localization.sec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :
R × M

Given a localization map f : M →* N, a section function sending z : N to some (x, y) : M × S such that f x * (f y)⁻¹ = z.

Equations
theorem is_localization.sec_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :

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

theorem is_localization.sec_spec' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :

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

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

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

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

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

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

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

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

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

Equations
theorem is_localization.lift_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) (y : M) :

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

theorem is_localization.lift_mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) (v : P) (y : M) :
@[simp]
theorem is_localization.lift_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) :
theorem is_localization.lift_eq_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {x y : R × M} :
@[simp]
theorem is_localization.lift_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
@[simp]
theorem is_localization.lift_of_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (j : S →+* P) :
theorem is_localization.epic_of_localization_map {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] (j k : S →+* P) (h : ∀ (a : R), (j.comp (algebra_map R S)) a = (k.comp (algebra_map R S)) a) :
j = k
theorem is_localization.lift_unique {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {j : S →+* P} (hj : ∀ (x : R), j ((algebra_map R S) x) = g x) :
@[simp]
theorem is_localization.lift_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : S) :
theorem is_localization.lift_surjective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
function.surjective (is_localization.lift hg) ∀ (v : P), ∃ (x : R × M), v * g (x.snd) = g x.fst
theorem is_localization.lift_injective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
def is_localization.map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (g : R →+* P) (hy : M submonoid.comap g T) :
S →+* Q

Map a homomorphism g : R →+* P to S →+* Q, where S and Q are localizations of R and P at M and T respectively, such that g(M) ⊆ T.

We send z : S to algebra_map P Q (g x) * (algebra_map P Q (g y))⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

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

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

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

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

@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom M = T) (ᾰ : S) :
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_symm_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom M = T) (ᾰ : Q) :
def is_localization.ring_equiv_of_ring_equiv {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [algebra P Q] [is_localization T Q] (h : R ≃+* P) (H : submonoid.map h.to_monoid_hom M = T) :
S ≃+* Q

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

Equations
theorem is_localization.ring_equiv_of_ring_equiv_eq_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) :
@[simp]
theorem is_localization.ring_equiv_of_ring_equiv_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) :
theorem is_localization.ring_equiv_of_ring_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] [is_localization M S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [algebra P Q] [is_localization T Q] {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) (y : M) :
def is_localization.alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] :

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

Equations
@[simp]
theorem is_localization.alg_equiv_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] (ᾰ : S) :
@[simp]
theorem is_localization.alg_equiv_symm_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (Q : Type u_4) [comm_ring Q] [algebra R Q] [is_localization M Q] (ᾰ : Q) :
@[simp]
theorem is_localization.alg_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_ring Q] [algebra R Q] [is_localization M Q] (x : R) (y : M) :
@[simp]
theorem is_localization.alg_equiv_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {Q : Type u_4} [comm_ring Q] [algebra R Q] [is_localization M Q] (x : R) (y : M) :
def is_localization.away {R : Type u_1} [comm_ring R] (x : R) (S : Type u_2) [comm_ring S] [algebra R S] :
Prop

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

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

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

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

Given x : R, a localization map F : R →+* S away from x, and a map of comm_rings g : R →+* P such that g x is invertible, the homomorphism induced from S to P sending z : S to g y * (g x)⁻ⁿ, where y : R, n : ℕ are such that z = F y * (F x)⁻ⁿ.

Equations
@[simp]
theorem is_localization.away.away_map.lift_eq {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (g x)) (a : R) :
@[simp]
theorem is_localization.away.away_map.lift_comp {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (g x)) :
def is_localization.away.away_to_away_right {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (x : R) [is_localization.away x S] (y : R) [algebra R P] [is_localization.away (x * y) P] :
S →+* P

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

Equations

Constructing a localization at a given submonoid #

@[instance]
def localization.has_add {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[instance]
def localization.has_neg {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[instance]
def localization.has_zero {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[instance]
def localization.comm_ring {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[instance]
def localization.algebra {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[instance]
theorem localization.mk_one_eq_algebra_map {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) :
theorem localization.mk_eq_mk'_apply {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) (y : M) :
def localization.alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

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

Equations
@[simp]
@[simp]
theorem localization.alg_equiv_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (ᾰ : localization M) :
@[simp]
theorem localization.alg_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
@[simp]
theorem localization.alg_equiv_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem localization.alg_equiv_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
theorem localization.alg_equiv_symm_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : R) (y : M) :
def ideal.prime_compl {R : Type u_1} [comm_ring R] (I : ideal R) [hp : I.is_prime] :

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

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

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

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

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

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

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

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

If S is the localization of R at a submonoid, the ordering of ideals of S is embedded in the ordering of ideals of R.

Equations

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M. This lemma gives the particular case for an ideal and its comap, see le_rel_iso_of_prime for the more general relation isomorphism

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

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M. This lemma gives the particular case for an ideal and its map, see le_rel_iso_of_prime for the more general relation isomorphism, and the reverse implication

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

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M

Equations

quotient_map applied to maximal ideals of a localization is surjective. The quotient by a maximal ideal is a field, so inverses to elements already exist, and the localization necessarily maps the equivalence class of the inverse in the localization

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

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

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

coeff_integer_normalization p gives the coefficients of the polynomial integer_normalization p

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

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

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

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

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

Equations

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

Equations
@[instance]

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

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

The unique maximal ideal of the localization at I.prime_compl lies over the ideal I.

The image of I in the localization at I.prime_compl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure at_prime.local_ring

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

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

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

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

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

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

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

@[instance]

The cast from int to rat as a fraction_ring.

theorem is_fraction_ring.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] {x : R} :
(algebra_map R K) x = 0 x = 0
theorem is_fraction_ring.injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] [is_fraction_ring R K] :
theorem is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] [nontrivial R] {x : R} (hx : x non_zero_divisors R) :
def is_fraction_ring.to_integral_domain (A : Type u_4) [integral_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :

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

Equations
def is_fraction_ring.inv (A : Type u_4) [integral_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] (z : K) :
K

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

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

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

Equations
theorem is_fraction_ring.mk'_mk_eq_div {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r s : A} (hs : s non_zero_divisors A) :
theorem is_fraction_ring.mk'_eq_div {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r : A} (s : (non_zero_divisors A)) :
theorem is_fraction_ring.is_unit_map_of_injective {A : Type u_4} [integral_domain A] {L : Type u_7} [field L] {g : A →+* L} (hg : function.injective g) (y : (non_zero_divisors A)) :
def is_fraction_ring.lift {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) :
K →+* L

Given an integral domain A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, we get a field hom sending z : K to g x * (g y)⁻¹, where (x, y) : A × (non_zero_divisors A) are such that z = f x * (f y)⁻¹.

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

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

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

Given integral domains A, B with fields of fractions K, L and an injective ring hom j : A →+* B, we get a field hom sending z : K to g (j x) * (g (j y))⁻¹, where (x, y) : A × (non_zero_divisors A) are such that z = f x * (f y)⁻¹.

Equations
def is_fraction_ring.field_equiv_of_ring_equiv {A : Type u_4} [integral_domain A] {K : Type u_5} {B : Type u_6} [integral_domain B] [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra B L] [is_fraction_ring B L] (h : A ≃+* B) :
K ≃+* L

Given integral domains A, B and localization maps to their fields of fractions f : A →+* K, g : B →+* L, an isomorphism j : A ≃+* B induces an isomorphism of fields of fractions K ≃+* L.

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

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

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

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

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

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

Equations
theorem is_fraction_ring.num_denom_reduced (A : Type u_4) [integral_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] (x : K) {d : A} :
theorem is_fraction_ring.eq_zero_of_num_eq_zero {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] [unique_factorization_monoid A] {x : K} (h : is_fraction_ring.num A x = 0) :
x = 0
def localization_algebra {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] :
algebra Rₘ Sₘ

Definition of the natural algebra induced by the localization of an algebra. Given an algebra R → S, a submonoid R of M, and a localization Rₘ for M, let Sₘ be the localization of S to the image of M under algebra_map R S. Then this is the natural algebra structure on Rₘ → Sₘ, such that the entire square commutes, where localization_map.map_comp gives the commutativity of the underlying maps

Equations
theorem algebra_map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] (r : R) (m : M) :
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_6) (Sₘ : Type u_7) [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] (hRS : function.injective (algebra_map R S)) (hM : algebra.algebra_map_submonoid S M non_zero_divisors S) :

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

theorem ring_hom.is_integral_elem_localization_at_leading_coeff {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (x : S) (p : polynomial R) (hf : polynomial.eval₂ f x p = 0) (M : submonoid R) (hM : p.leading_coeff M) {Rₘ : Type u_3} {Sₘ : Type u_4} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (submonoid.map f M) Sₘ] :
theorem is_integral_localization_at_leading_coeff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] {x : S} (p : polynomial R) (hp : (polynomial.aeval x) p = 0) (hM : p.leading_coeff M) :

Given a particular witness to an element being algebraic over an algebra R → S, We can localize to a submonoid containing the leading coefficient to make it integral. Explicitly, the map between the localizations will be an integral ring morphism

theorem is_integral_localization {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [algebra R S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R Rₘ] [is_localization M Rₘ] [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] (H : algebra.is_integral R S) :

If R → S is an integral extension, M is a submonoid of R, Rₘ is the localization of R at M, and Sₘ is the localization of S at the image of M under the extension map, then the induced map Rₘ → Sₘ is also an integral extension

theorem is_integral_localization' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : f.is_integral) (M : submonoid R) :
theorem integral_closure.is_fraction_ring_of_algebraic {A : Type u_4} [integral_domain A] {L : Type u_6} [field L] [algebra A L] (alg : algebra.is_algebraic A L) (inj : ∀ (x : A), (algebra_map A L) x = 0x = 0) :

If the field L is an algebraic extension of the integral domain A, the integral closure of A in L has fraction field L.

theorem integral_closure.is_fraction_ring_of_finite_extension {A : Type u_4} [integral_domain A] (K : Type u_5) (L : Type u_6) [field K] [field L] [algebra A K] [is_fraction_ring A K] [algebra A L] [algebra K L] [is_scalar_tower A K L] [finite_dimensional K L] :

If the field L is a finite extension of the fraction field of the integral domain A, the integral closure of A in L has fraction field L.

def fraction_ring (A : Type u_4) [integral_domain A] :
Type u_4

The fraction field of an integral domain as a quotient type.

Equations
@[simp]
def fraction_ring.alg_equiv (A : Type u_4) [integral_domain A] (K : Type u_1) [field K] [algebra A K] [is_fraction_ring A K] :

Given an integral domain A and a localization map to a field of fractions f : A →+* K, we get an A-isomorphism between the field of fractions of A as a quotient type and K.

Equations