# mathlibdocumentation

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 #

• `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
• `is_localization.is_integer` is a predicate stating that `x : S` is in the image of `R`
• `is_localization.away (x : R) S` expresses that `S` is a localization away from `x`, as an abbreviation of `is_localization (submonoid.powers x) S`
• `is_localization.at_prime (I : ideal R) [is_prime I] (S : Type*)` expresses that `S` is a localization at (the complement of) a prime ideal `I`, as an abbreviation of `is_localization I.prime_compl S`
• `is_fraction_ring R K` expresses that `K` is a field of fractions of `R`, as an abbreviation of `is_localization (non_zero_divisors R) K`

## 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
• `is_localization.at_prime.local_ring`: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring
• `is_fraction_ring.field`: a definition (not an instance) stating the localization of an integral domain `R` at `R \ {0}` is a field
• `rat.is_fraction_ring` is an instance stating `ℚ` is the field of fractions of `ℤ`

## 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} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ 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
theorem is_localization.of_le {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (N : submonoid R) (h₁ : M N) (h₂ : ∀ (r : R), r Nis_unit ( S) r)) :
def is_localization.to_localization_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ 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_monoid_hom_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (ᾰ : R) :
= S)
@[simp]
theorem is_localization.to_localization_map_to_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :
theorem is_localization.to_localization_map_to_map_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (x : R) :
= S) x
def is_localization.is_integer (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ 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] [ S] :
theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem is_localization.is_integer_add {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a + b)
theorem is_localization.is_integer_mul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a * b)
theorem is_localization.is_integer_smul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a : R} {b : S} (hb : b) :
(a b)
theorem is_localization.exists_integer_multiple' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (a : S) :
∃ (b : M), (a * S) b)

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] [ S] [ S] (a : S) :
∃ (b : M), (b a)

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

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

noncomputable def is_localization.sec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] :
theorem is_localization.sec_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ 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.exist_integer_multiples {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι → S) :
∃ (b : M), ∀ (i : ι), i s (b f i)

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
theorem is_localization.finset_integer_multiple_image {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] [decidable_eq R] (s : finset S) :
theorem is_localization.map_right_cancel {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (r : R) :
S) r = 0 ∃ (m : M), r * m = 0
noncomputable def is_localization.mk' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (z : S) :
z).snd = z
theorem is_localization.mk'_mul {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (x₁ x₂ : R) (y₁ y₂ : M) :
(x₁ * x₂) (y₁ * y₂) = x₁ y₁) * y₂
theorem is_localization.mk'_one {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (x : R) :
1 = S) x
@[simp]
theorem is_localization.mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (x : R) (y : M) :
y) * S) y = S) x
@[simp]
theorem is_localization.mk'_spec' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (x : R) (y : M) :
( S) y) * y = S) x
@[simp]
theorem is_localization.mk'_spec_mk {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] {x : R} {y : M} {z : S} :
y = z S) x = z * S) y
theorem is_localization.mk'_surjective {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (z : S) :
∃ (x : R) (y : M), 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] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] {x : R} {y : M} {I : ideal S} :
y I S) x I
@[protected]
theorem is_localization.eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] {a₁ b₁ : R} {a₂ b₂ : M} :
a₂ = 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] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] [ P] [ P] {x₁ x₂ : R} {y₁ y₂ : M} :
y₁ = y₂ y₁ = 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] [ 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} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] {x : R} (hx : x M) :
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] [ S] [ S] {x : M} :
x = 1
theorem is_localization.mk'_self'' {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] {x : M} :
x = 1
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] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : R) (y : M) :
y = ( S) x) * y
@[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] [ S] [ S] (x : R) (y : M) :
((y) * x) y = S) x
theorem is_localization.mk'_mul_cancel_right {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : R) (y : M) :
(x * y) y = S) x
@[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] [ S] [ S] (x y : M) :
y) * x = 1
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] [ S] [ S] (x : R) (y : M) (h : x M) :
y) * x, h⟩ = 1
theorem is_localization.is_unit_comp {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] (j : S →+* P) (y : M) :
is_unit ((j.comp S)) y)
theorem is_localization.eq_of_eq {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] {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_ring`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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x₁ x₂ : R) (y₁ y₂ : M) :
(x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = y₁ + y₂
noncomputable def is_localization.lift {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] {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_ring`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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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_ring`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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] (j : S →+* P) :
theorem is_localization.monoid_hom_ext {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] ⦃j k : S →* P⦄ (h : j.comp S) = k.comp S)) :
j = k
theorem is_localization.ring_hom_ext {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] ⦃j k : S →+* P⦄ (h : j.comp S) = k.comp S)) :
j = k
@[protected]
theorem is_localization.ext {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] (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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : S) :
= x
theorem is_localization.lift_surjective_iff {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] {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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M ) [ Q] [ Q] (x : R) :
hy) ( S) x) = Q) (g x)
@[simp]
theorem is_localization.map_comp {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] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M ) [ Q] [ Q] :
hy).comp S) = Q).comp g
theorem is_localization.map_mk' {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] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M ) [ Q] [ Q] (x : R) (y : M) :
hy) y) = (g x) g y, _⟩
@[simp]
theorem is_localization.map_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (z : S) (h : M := _) :
h) z = z
theorem is_localization.map_unique {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] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {g : R →+* P} {T : submonoid P} {Q : Type u_4} [comm_ring Q] (hy : M ) [ Q] [ Q] {A : Type u_5} [comm_ring A] {U : submonoid A} {W : Type u_6} [comm_ring W] [ W] [ W] {l : P →+* A} (hl : T ) :
hl).comp hy) = (l.comp g) _

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

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] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [ Q] [ Q] (h : R ≃+* P) (H : = 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] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [ 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} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} (Q : Type u_4) [comm_ring Q] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [ Q] [ Q] {j : R ≃+* P} (H : = 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] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [ 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} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] {T : submonoid P} {Q : Type u_4} [comm_ring Q] [ 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} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (Q : Type u_4) [comm_ring Q] [ 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} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (Q : Type u_4) [comm_ring Q] [ Q] [ Q] (ᾰ : S) :
Q) =
@[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] [ S] [ S] (Q : Type u_4) [comm_ring Q] [ Q] [ Q] (ᾰ : Q) :
Q).symm) =
@[simp]
theorem is_localization.alg_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] {Q : Type u_4} [comm_ring Q] [ Q] [ Q] (x : R) (y : M) :
Q) y) = y
@[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] [ S] [ S] {Q : Type u_4} [comm_ring Q] [ Q] [ Q] (x : R) (y : M) :
Q).symm) y) = y
theorem is_localization.is_localization_of_alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ P] [ S] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ P] (h : S ≃ₐ[R] P) :
theorem is_localization.is_localization_iff_of_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] {P : Type u_3} [comm_ring P] (h : S ≃+* P) :
theorem is_localization.is_localization_of_base_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] {P : Type u_3} [comm_ring P] [ S] (h : R ≃+* P) :
theorem is_localization.is_localization_iff_of_base_ring_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
def is_localization.away {R : Type u_1} [comm_ring R] (x : R) (S : Type u_2) [comm_ring S] [ S] :
Prop

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

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

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

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

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

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

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

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

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

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

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

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

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

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

### Constructing a localization at a given submonoid #

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

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

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

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

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

Equations
• 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]
def localization.zero {R : Type u_1} [comm_ring R] {M : submonoid R} :

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

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

Equations
@[protected, instance]
def localization.has_zero {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
theorem localization.mk_zero {R : Type u_1} [comm_ring R] {M : submonoid R} (b : M) :
= 0
@[protected, instance]
def localization.comm_ring {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[protected, instance]
def localization.distrib_mul_action {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [monoid S] [ R] [ R] :
Equations
@[protected, instance]
def localization.mul_semiring_action {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [semiring S] [ R] [ R] :
Equations
@[protected, instance]
def localization.module {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [semiring S] [ R] [ R] :
Equations
@[protected, instance]
def localization.algebra {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [ R] :
Equations
@[protected, instance]
def localization.is_localization {R : Type u_1} [comm_ring R] {M : submonoid R} :
@[simp]
theorem localization.to_localization_map_eq_monoid_of {R : Type u_1} [comm_ring R] {M : submonoid R} :
theorem localization.monoid_of_eq_algebra_map {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) :
x = (localization M)) x
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) :
= y
@[simp]
theorem localization.mk_eq_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} :
noncomputable def localization.alg_equiv {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ 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} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (ᾰ : S) :
S).symm) = ((ring_equiv.refl R).symm) _)
@[simp]
theorem localization.alg_equiv_apply {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ 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] [ S] [ S] (x : R) (y : M) :
y) = y
@[simp]
theorem localization.alg_equiv_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : R) (y : M) :
S).symm) y) = y
theorem localization.alg_equiv_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : R) (y : M) :
y) = y
theorem localization.alg_equiv_symm_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (x : R) (y : M) :
S).symm) y) =
noncomputable def localization.away_lift {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (f : R →+* P) (r : R) (hr : is_unit (f r)) :

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

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

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

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

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

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

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

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

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

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

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] [ S] [ S] {I : ideal R} {z : S} :
z ideal.map S) I ∃ (x : I × M), z * S) (x.snd) = 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] [ S] [ S] (J : ideal S) :
ideal.map S) (ideal.comap S) J) = J
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] [ S] [ S] (I : ideal R) (hI : I.is_prime) (hM : I) :
ideal.comap S) (ideal.map S) I) = I
def is_localization.order_embedding {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ 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
theorem is_localization.is_prime_iff_is_prime_disjoint {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (J : ideal S) :

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] [ S] [ S] (I : ideal R) (hp : I.is_prime) (hd : 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] [ S] [ S] :
{p // p.is_prime} ≃o {p // p.is_prime 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
theorem is_localization.surjective_quotient_map_of_maximal_of_localization {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] {I : ideal S} [I.is_prime] {J : ideal R} {H : J ideal.comap S) I} (hI : (ideal.comap S) I).is_maximal) :

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

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

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

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

The localization away from a unit is isomorphic to the ring

Equations
• e = _
noncomputable def is_localization.at_one (R : Type u_1) [comm_ring R] (S : Type u_2) [comm_ring S] [ S] [ S] :

The localization at one is isomorphic to the ring.

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

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

Equations
@[simp]
theorem is_localization.mem_localization_localization_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] {N : submonoid S} {x : R} :
∃ (y : N) (z : M), S) x = (y) * S) z
theorem is_localization.localization_localization_map_units {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ T]  :
theorem is_localization.localization_localization_surj {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ T] (x : T) :
∃ (y : , x * T) (y.snd) = T) y.fst
theorem is_localization.localization_localization_eq_iff_exists {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ T] (x y : R) :
T) x = T) y ∃ (c : , x * c = y * c
theorem is_localization.localization_localization_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ T] :

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

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

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

theorem is_localization.is_localization_is_localization_at_prime_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (T : Type u_4) [comm_ring T] [ T] [ T] [ T] (p : ideal S) [Hp : p.is_prime]  :
(ideal.comap S) p)

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

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

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

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

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

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

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

@[protected, instance]
noncomputable def is_localization.localization.algebra {R : Type u_1} [comm_ring R] (x : ideal R) [H : x.is_prime] [is_domain R] :
Equations
theorem is_localization.is_localization_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (T : Type u_4) [comm_ring T] [ T] (M N : submonoid R) (h : M N) [ S] [ T] [ T] [ T] :
T

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

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

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

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

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] [ S] (I : ideal R) {x : S} :
∃ (y : R), y I S) y = x
theorem is_localization.coe_submodule_mono {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ 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] [ S] :
@[simp]
theorem is_localization.coe_submodule_top {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] :
@[simp]
theorem is_localization.coe_submodule_sup {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (I J : ideal R) :
@[simp]
theorem is_localization.coe_submodule_mul {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (I J : ideal R) :
theorem is_localization.coe_submodule_fg {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (hS : function.injective S)) (I : ideal R) :
@[simp]
theorem is_localization.coe_submodule_span {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (s : set R) :
= ( S) '' s)
@[simp]
theorem is_localization.coe_submodule_span_singleton {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (x : R) :
= { S) x}
theorem is_localization.map_smul {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] {g : R →+* P} {T : submonoid P} (hy : M ) {Q : Type u_4} [comm_ring Q] [ Q] [ Q] (x : S) (z : R) :
hy) (z x) = g z hy) x
theorem is_localization.is_noetherian_ring {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (h : is_noetherian_ring R) :
noncomputable def is_localization.coeff_integer_normalization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) (i : ) :
R

`coeff_integer_normalization p` gives the coefficients of the polynomial `integer_normalization p`

Equations
theorem is_localization.coeff_integer_normalization_of_not_mem_support {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) (i : ) (h : p.coeff i = 0) :
theorem is_localization.coeff_integer_normalization_mem_support {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) (i : ) (h : 0) :
noncomputable def is_localization.integer_normalization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) :

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

Equations
@[simp]
theorem is_localization.integer_normalization_coeff {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) (i : ) :
theorem is_localization.integer_normalization_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) :
∃ (b : M), ∀ (i : ), S) = b p.coeff i
theorem is_localization.integer_normalization_map_to_map {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) :
∃ (b : M), = b p
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] [ S] [ S] {R' : Type u_5} [comm_ring R'] (g : S →+* R') (p : polynomial S) {x : R'} (hx : 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] [ S] [ S] {R' : Type u_5} [comm_ring R'] [ R'] [ R'] [ R'] (p : polynomial S) {x : R'} (hx : 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] [ S] [ S] {x : R} (hM : M R) :
S) x = 0 x = 0
@[protected]
theorem is_localization.injective {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (hM : M R) :
@[protected]
theorem is_localization.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] [nontrivial R] (hM : M R) {x : R} (hx : x R) :
S) x 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] {g : R →+* P} (Q : Type u_4) [comm_ring Q] [ Q] (hg : function.injective g) [ Q] (hM : P) :

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

theorem is_localization.coe_submodule_le_coe_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (h : M R) {I J : ideal R} :
theorem is_localization.coe_submodule_strict_mono {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] [ S] (h : M R) :
theorem is_localization.coe_submodule_injective {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] (h : M R) :
theorem is_localization.coe_submodule_is_principal {R : Type u_1} [comm_ring R] {M : submonoid R} (S : Type u_2) [comm_ring S] [ S] [ S] {I : ideal R} (h : M R) :
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) :

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

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

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

@[protected, instance]
def is_localization.is_domain_of_local_at_prime {A : Type u_6} [comm_ring A] [is_domain A] {P : ideal A} (hp : P.is_prime) :

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

theorem is_localization.at_prime.is_unit_to_map_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (I : ideal R) [hI : I.is_prime] (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] [ S] (I : ideal R) [hI : I.is_prime] (x : R) (h : := _) :
S) x x I
theorem is_localization.at_prime.is_unit_mk'_iff {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (I : ideal R) [hI : I.is_prime] (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] [ S] (I : ideal R) [hI : I.is_prime] (x : R) (y : (I.prime_compl)) (h : := _) :
x I
theorem localization.at_prime.comap_maximal_ideal {R : Type u_1} [comm_ring R] {I : ideal R} [hI : I.is_prime] :

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

theorem localization.at_prime.map_eq_maximal_ideal {R : Type u_1} [comm_ring R] {I : ideal R} [hI : I.is_prime] :

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} :
J I
noncomputable def localization.local_ring_hom {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = 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
• hIJ =
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 = J) (x : R) :
hIJ) ( x) = (f x)
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 = J) (x : R) (y : (I.prime_compl)) :
hIJ) y) = f y, _⟩
@[protected, instance]
def localization.is_local_ring_hom_local_ring_hom {R : Type u_1} [comm_ring R] {P : Type u_3} [comm_ring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = 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 = J) (hj : ∀ (x : R), j ( x) = (f x)) :
hIJ = j
@[simp]
theorem localization.local_ring_hom_id {R : Type u_1} [comm_ring R] (I : ideal R) [hI : I.is_prime] :
@[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 = J) (g : S →+* P) (hJK : J = K) :
(g.comp f) _ = hJK).comp hIJ)
theorem localization_map_bijective_of_field {R : Type u_1} {Rₘ : Type u_2} [comm_ring R] [is_domain R] [comm_ring Rₘ] {M : submonoid R} (hM : 0 M) (hR : is_field R) [ Rₘ] [ 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] [ K] :
Prop

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

@[protected, instance]

The cast from `int` to `rat` as a `fraction_ring`.

theorem is_fraction_ring.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K] {x : R} :
K) x = 0 x = 0
@[protected]
theorem is_fraction_ring.injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [ K] [ K] :
@[simp]
theorem is_fraction_ring.coe_submodule_le_coe_submodule {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K] {I J : ideal R} :
theorem is_fraction_ring.coe_submodule_strict_mono {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K] :
@[protected, instance]
def is_fraction_ring.no_zero_smul_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K]  :
theorem is_fraction_ring.coe_submodule_injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [ K] [ K] :
@[simp]
theorem is_fraction_ring.coe_submodule_is_principal (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [ K] [ K] {I : ideal R} :
@[protected]
theorem is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K] [nontrivial R] {x : R} (hx : x R) :
K) x 0
@[protected]
theorem is_fraction_ring.is_domain (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [ K] [ K] :

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

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

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

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

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

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

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

Equations
@[simp]
theorem is_fraction_ring.lift_algebra_map {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [ K] [ K] {g : A →+* L} (hg : function.injective g) (x : A) :
( K) x) = g x

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

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

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

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

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

Equations
noncomputable def is_fraction_ring.field_equiv_of_ring_equiv {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} {B : Type u_6} [comm_ring B] [is_domain B] [field K] {L : Type u_7} [field L] [ K] [ K] [ L] [ 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.integer_normalization_eq_zero_iff {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {p : polynomial K} :
p = 0
theorem is_fraction_ring.is_algebraic_iff (A : Type u_4) [comm_ring A] [is_domain A] (K : Type u_5) [field K] {L : Type u_7} [field L] [ K] [ K] [ L] [ L] [ L] {x : L} :
x x

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

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

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

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

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

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

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

Equations
theorem is_fraction_ring.num_denom_reduced (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] (x : K) {d : A} :
d
@[simp]
theorem is_fraction_ring.mk'_num_denom (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] (x : K) :
= x
theorem is_fraction_ring.num_mul_denom_eq_num_iff_eq {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x y : K} :
x * K) = K) y) x = y
theorem is_fraction_ring.num_mul_denom_eq_num_iff_eq' {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x y : K} :
y * K) = K) x) x = y
theorem is_fraction_ring.num_mul_denom_eq_num_mul_denom_iff_eq {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x y : K} :
y) * = x) * x = y
theorem is_fraction_ring.eq_zero_of_num_eq_zero {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x : K} (h : = 0) :
x = 0
theorem is_fraction_ring.is_integer_of_is_unit_denom {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x : K} (h : is_unit ) :
theorem is_fraction_ring.is_unit_denom_of_num_eq_zero {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [ K] [ K] {x : K} (h : = 0) :
theorem is_fraction_ring.is_fraction_ring_iff_of_base_ring_equiv {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
noncomputable def localization_algebra {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] {Rₘ : Type u_6} {Sₘ : Type u_7} [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

Equations
theorem algebra_map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [