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.

Given such a localization map f : R →+* S, we can define the surjection localization_map.mk' sending (x, y) : R × M to f x * (f y)⁻¹, and localization_map.lift, the homomorphism from S induced by a homomorphism from R which maps elements of M to invertible elements of the codomain. Similarly, given commutative rings P, Q, a submonoid T of P and a localization map for T from P to Q, then a homomorphism g : R →+* P such that g(M) ⊆ T induces a homomorphism of localizations, localization_map.map, from S to Q. We treat the special case of localizing away from an element in the sections away_map and away.

We show the localization as a quotient type, defined in group_theory.monoid_localization as submonoid.localization, is a comm_ring and that the natural ring hom of : R →+* localization M is a localization map.

We show that a localization at the complement of a prime ideal is a local ring.

We prove some lemmas about the R-algebra structure of S.

When R is an integral domain, we define fraction_map R K as an abbreviation for localization (non_zero_divisors R) K, the natural map to R's field of fractions.

We show that a comm_ring K which is the localization of an integral domain R at R \ {0} is a field. We use this to show the field of fractions as a quotient type, fraction_ring, is a field.

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 ring localization map is defined to be a localization map of the underlying comm_monoid (a submonoid.localization_map) which is also a ring hom. To prove most lemmas about a localization_map f in this file we invoke the corresponding proof for the underlying comm_monoid localization map f.to_localization_map, which can be found in group_theory.monoid_localization and the namespace submonoid.localization_map.

To apply a localization map f as a function, we use f.to_map, as coercions don't work well for this structure.

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 of : localization_map M (localization M) (where of establishes the localization as a quotient type satisfies the characteristic predicate). 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.

We define a copy of the localization map f's codomain S carrying the data of f so that instances on S induced by f can 'know' the map needed to induce the instance.

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

def localization_map.to_localization_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :

The comm_monoid localization_map underlying a comm_ring localization_map. See group_theory.monoid_localization for its definition.

@[nolint]
structure localization_map {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] :
Type (max u_1 u_2)

The type of ring homomorphisms satisfying the characteristic predicate: if f : R →+* S satisfies this predicate, then S is isomorphic to the localization of R at M. We later define an instance coercing a localization map f to its codomain S so that instances on S induced by f can 'know' the map needed to induce the instance.

def localization_map.to_ring_hom {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :

The ring hom underlying a localization_map.

def ring_hom.to_localization_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : R →+* S) :
(∀ (y : M), is_unit (f y))(∀ (z : S), ∃ (x : R × M), z * f (x.snd) = f x.fst)(∀ (x y : R), f x = f y ∃ (c : M), x * c = y * c)localization_map M S

Makes a localization map from a comm_ring hom satisfying the characteristic predicate.

Equations
def submonoid.localization_map.to_ring_localization {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : M.localization_map S) :
(∀ (x y : R), (f.to_map) (x + y) = (f.to_map) x + (f.to_map) y)localization_map M S

Makes a comm_ring localization map from an additive comm_monoid localization map of comm_rings.

Equations
@[nolint]
def localization_map.codomain {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :
localization_map M SType u_2

We define a copy of the localization map f's codomain S carrying the data of f so that instances on S induced by f can 'know` the map needed to induce the instance.

Equations
@[instance]
def localization_map.comm_ring {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

Equations
@[instance]
def localization_map.field {R : Type u_1} [comm_ring R] {M : submonoid R} {K : Type u_2} [field K] (f : localization_map M K) :

Equations
def localization_map.to_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :

Short for to_ring_hom; used for applying a localization map as a function.

theorem localization_map.map_units {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (y : M) :

theorem localization_map.surj {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (z : S) :
∃ (x : R × M), z * (f.to_map) (x.snd) = (f.to_map) x.fst

theorem localization_map.eq_iff_exists {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x y : R} :
(f.to_map) x = (f.to_map) y ∃ (c : M), x * c = y * c

@[ext]
theorem localization_map.ext {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f g : localization_map M S} :
(∀ (x : R), (f.to_map) x = (g.to_map) x)f = g

theorem localization_map.ext_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f g : localization_map M S} :
f = g ∀ (x : R), (f.to_map) x = (g.to_map) x

def localization_map.is_integer {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :
localization_map M SS → Prop

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

Equations
theorem localization_map.is_integer_add {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {a b : S} :
f.is_integer af.is_integer bf.is_integer (a + b)

theorem localization_map.is_integer_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {a b : S} :
f.is_integer af.is_integer bf.is_integer (a * b)

theorem localization_map.is_integer_smul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {a : R} {b : S} :
f.is_integer bf.is_integer (((f.to_map) a) * b)

theorem localization_map.exists_integer_multiple' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (a : S) :
∃ (b : M), f.is_integer (a * (f.to_map) 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 localization_map.exists_integer_multiple {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (a : S) :
∃ (b : M), f.is_integer (((f.to_map) 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.

theorem localization_map.sec_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (z : S) :

Given z : S, f.to_localization_map.sec 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 localization_map.sec_spec' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (z : S) :

Given z : S, f.to_localization_map.sec 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 localization_map.exist_integer_multiples_of_finset {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (s : finset S) :
∃ (b : M), ∀ (a : S), a sf.is_integer (((f.to_map) b) * a)

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

theorem localization_map.map_right_cancel {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x y : R} {c : M} :
(f.to_map) ((c) * x) = (f.to_map) ((c) * y)(f.to_map) x = (f.to_map) y

theorem localization_map.map_left_cancel {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x y : R} {c : M} :
(f.to_map) (x * c) = (f.to_map) (y * c)(f.to_map) x = (f.to_map) y

theorem localization_map.eq_zero_of_fst_eq_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {z : S} {x : R} {y : M} :
z * (f.to_map) y = (f.to_map) xx = 0z = 0

def localization_map.mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :
localization_map M SR → M → S

Given a localization map f : R →+* S, the surjection sending (x, y) : R × M to f x * (f y)⁻¹.

Equations
@[simp]
theorem localization_map.mk'_sec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (z : S) :

theorem localization_map.mk'_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x₁ x₂ : R) (y₁ y₂ : M) :
f.mk' (x₁ * x₂) (y₁ * y₂) = (f.mk' x₁ y₁) * f.mk' x₂ y₂

theorem localization_map.mk'_one {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) :
f.mk' x 1 = (f.to_map) x

@[simp]
theorem localization_map.mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) :
(f.mk' x y) * (f.to_map) y = (f.to_map) x

@[simp]
theorem localization_map.mk'_spec' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) :
((f.to_map) y) * f.mk' x y = (f.to_map) x

theorem localization_map.eq_mk'_iff_mul_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : R} {y : M} {z : S} :
z = f.mk' x y z * (f.to_map) y = (f.to_map) x

theorem localization_map.mk'_eq_iff_eq_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : R} {y : M} {z : S} :
f.mk' x y = z (f.to_map) x = z * (f.to_map) y

theorem localization_map.mk'_surjective {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (z : S) :
∃ (x : R) (y : M), f.mk' x y = z

theorem localization_map.mk'_eq_iff_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x₁ x₂ : R} {y₁ y₂ : M} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ (f.to_map) (x₁ * y₂) = (f.to_map) (x₂ * y₁)

theorem localization_map.mk'_mem_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : R} {y : M} {I : ideal S} :
f.mk' x y I (f.to_map) x I

theorem localization_map.eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {a₁ b₁ : R} {a₂ b₂ : M} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ ∃ (c : M), (a₁ * b₂) * c = (b₁ * a₂) * c

theorem localization_map.eq_iff_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) (g : localization_map M P) {x y : R} :
(f.to_map) x = (f.to_map) y (g.to_map) x = (g.to_map) y

theorem localization_map.mk'_eq_iff_mk'_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) (g : localization_map M P) {x₁ x₂ : R} {y₁ y₂ : M} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ g.mk' x₁ y₁ = g.mk' x₂ y₂

theorem localization_map.mk'_eq_of_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {a₁ b₁ : R} {a₂ b₂ : M} :
b₁ * a₂ = a₁ * b₂f.mk' a₁ a₂ = f.mk' b₁ b₂

@[simp]
theorem localization_map.mk'_self {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : R} (hx : x M) :
f.mk' x x, hx⟩ = 1

@[simp]
theorem localization_map.mk'_self' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : M} :
f.mk' x x = 1

theorem localization_map.mk'_self'' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : M} :
f.mk' x.val x = 1

theorem localization_map.mul_mk'_eq_mk'_of_mul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x y : R) (z : M) :
((f.to_map) x) * f.mk' y z = f.mk' (x * y) z

theorem localization_map.mk'_eq_mul_mk'_one {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) :
f.mk' x y = ((f.to_map) x) * f.mk' 1 y

@[simp]
theorem localization_map.mk'_mul_cancel_left {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) :
f.mk' ((y) * x) y = (f.to_map) x

theorem localization_map.mk'_mul_cancel_right {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) :
f.mk' (x * y) y = (f.to_map) x

@[simp]
theorem localization_map.mk'_mul_mk'_eq_one {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x y : M) :
(f.mk' x y) * f.mk' y x = 1

theorem localization_map.mk'_mul_mk'_eq_one' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : R) (y : M) (h : x M) :
(f.mk' x y) * f.mk' y x, h⟩ = 1

theorem localization_map.is_unit_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) (j : S →+* P) (y : M) :

theorem localization_map.eq_of_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {x y : R} :
(f.to_map) x = (f.to_map) yg 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 localization_map.mk'_add {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x₁ x₂ : R) (y₁ y₂ : M) :
f.mk' (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂

def localization_map.lift {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} :
(∀ (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 localization_map.lift_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map 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 localization_map.lift_mk'_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) (v : P) (y : M) :
(f.lift hg) (f.mk' x y) = v g x = (g y) * v

@[simp]
theorem localization_map.lift_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) (x : R) :
(f.lift hg) ((f.to_map) x) = g x

theorem localization_map.lift_eq_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {x y : R × M} :
(f.lift hg) (f.mk' x.fst x.snd) = (f.lift hg) (f.mk' y.fst y.snd) g ((x.fst) * (y.snd)) = g ((y.fst) * (x.snd))

@[simp]
theorem localization_map.lift_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
(f.lift hg).comp f.to_map = g

@[simp]
theorem localization_map.lift_of_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) (j : S →+* P) :
f.lift _ = j

theorem localization_map.epic_of_localization_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {j k : S →+* P} :
(∀ (a : R), (j.comp f.to_map) a = (k.comp f.to_map) a)j = k

theorem localization_map.lift_unique {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) {j : S →+* P} :
(∀ (x : R), j ((f.to_map) x) = g x)f.lift hg = j

@[simp]
theorem localization_map.lift_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (x : S) :
(f.lift _) x = x

@[simp]
theorem localization_map.lift_left_inverse {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {k : localization_map M S} (z : S) :
(k.lift _) ((f.lift _) z) = z

Given two localization maps f : R →+* S, k : R →+* P for a submonoid M ⊆ R, the hom from P to S induced by f is left inverse to the hom from S to P induced by k.

theorem localization_map.lift_surjective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
function.surjective (f.lift hg) ∀ (v : P), ∃ (x : R × M), v * g (x.snd) = g x.fst

theorem localization_map.lift_injective_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} (hg : ∀ (y : M), is_unit (g y)) :
function.injective (f.lift hg) ∀ (x y : R), (f.to_map) x = (f.to_map) y g x = g y

def localization_map.map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] :

Given a comm_ring homomorphism g : R →+* P where for submonoids M ⊆ R, T ⊆ P we have g(M) ⊆ T, the induced ring homomorphism from the localization of R at M to the localization of P at T: if f : R →+* S and k : P →+* Q are localization maps for M and T respectively, we send z : S to k (g x) * (k (g y))⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations
theorem localization_map.map_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} (x : R) :
(f.map hy k) ((f.to_map) x) = (k.to_map) (g x)

@[simp]
theorem localization_map.map_comp {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} :
(f.map hy k).comp f.to_map = k.to_map.comp g

theorem localization_map.map_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} (x : R) (y : M) :
(f.map hy k) (f.mk' x y) = k.mk' (g x) g y, _⟩

@[simp]
theorem localization_map.map_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (z : S) :
(f.map _ f) z = z

theorem localization_map.map_comp_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {A : Type u_5} [comm_ring A] {U : submonoid A} {W : Type u_6} [comm_ring W] (j : localization_map U W) {l : P →+* A} (hl : ∀ (w : T), l w U) :
(k.map hl j).comp (f.map hy k) = f.map _ j

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 localization_map.map_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {A : Type u_5} [comm_ring A] {U : submonoid A} {W : Type u_6} [comm_ring W] (j : localization_map U W) {l : P →+* A} (hl : ∀ (w : T), l w U) (x : S) :
(k.map hl j) ((f.map hy k) x) = (f.map _ j) 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.

def localization_map.ring_equiv_of_ring_equiv {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {T : submonoid P} {Q : Type u_4} [comm_ring Q] (k : localization_map T Q) (h : R ≃+* P) :

Given localization maps f : R →+* S, k : P →+* Q for submonoids M, T respectively, an isomorphism j : R ≃+* P such that j(M) = T induces an isomorphism of localizations S ≃+* Q.

Equations
@[simp]
theorem localization_map.ring_equiv_of_ring_equiv_eq_map_apply {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {T : submonoid P} {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : S) :
(f.ring_equiv_of_ring_equiv k j H) x = (f.map _ k) x

theorem localization_map.ring_equiv_of_ring_equiv_eq_map {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {T : submonoid P} {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) :

@[simp]
theorem localization_map.ring_equiv_of_ring_equiv_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {T : submonoid P} {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) :

theorem localization_map.ring_equiv_of_ring_equiv_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (f : localization_map M S) {T : submonoid P} {Q : Type u_4} [comm_ring Q] {k : localization_map T Q} {j : R ≃+* P} (H : submonoid.map j.to_monoid_hom M = T) (x : R) (y : M) :
(f.ring_equiv_of_ring_equiv k j H) (f.mk' x y) = k.mk' (j x) j y, _⟩

def localization_map.away_map {R : Type u_1} [comm_ring R] (x : R) (S' : Type u_2) [comm_ring S'] :
Type (max u_1 u_2)

Given x : R, the type of homomorphisms f : R →* S such that S is isomorphic to the localization of R at the submonoid generated by x.

Equations
def localization_map.away_map.inv_self {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (x : R) :

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

Equations
def localization_map.away_map.lift {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] {g : R →+* P} (x : R) :

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 localization_map.away_map.lift_eq {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] {g : R →+* P} (x : R) (F : localization_map.away_map x S) (hg : is_unit (g x)) (a : R) :

@[simp]
theorem localization_map.away_map.lift_comp {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] {g : R →+* P} (x : R) (F : localization_map.away_map x S) (hg : is_unit (g x)) :

def localization_map.away_to_away_right {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] (x : R) (F : localization_map.away_map x S) (y : R) :

Given x y : R and localization maps F : R →+* S, G : R →+* P away from x and x * y respectively, the homomorphism induced from S to P.

Equations
@[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
def localization.of {R : Type u_1} [comm_ring R] (M : submonoid R) :

Natural hom sending x : R, R a comm_ring, to the equivalence class of (x, 1) in the localization of R at a submonoid.

Equations
theorem localization.monoid_of_eq_of {R : Type u_1} [comm_ring R] {M : submonoid R} (x : R) :

theorem localization.mk_one_eq_of {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) :

@[simp]
theorem localization.mk_eq_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} :

def localization.ring_equiv_of_quotient {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] :

Given a localization map f : R →+* S for a submonoid M, we get an isomorphism between the localization of R at M as a quotient type and S.

Equations
@[simp]

@[simp]
theorem localization.ring_equiv_of_quotient_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) (y : M) :

theorem localization.ring_equiv_of_quotient_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) (y : M) :

@[simp]
theorem localization.ring_equiv_of_quotient_of {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) :

@[simp]
theorem localization.ring_equiv_of_quotient_symm_mk' {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) (y : M) :

theorem localization.ring_equiv_of_quotient_symm_mk {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) (y : M) :

@[simp]
theorem localization.ring_equiv_of_quotient_symm_of {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (x : R) :

Given x : R, the natural hom sending y : R, R a comm_ring, to the equivalence class of (y, 1) in the localization of R at the submonoid generated by x.

Equations
def localization.away.ring_equiv_of_quotient {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (x : R) :

Given x : R and a localization map f : R →+* S away from x, we get an isomorphism between the localization of R at the submonoid generated by x as a quotient type and S.

Equations
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 localization_map.at_prime {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] (I : ideal R) [hp : I.is_prime] :
Type (max u_1 u_2)

A localization map from R to S where the submonoid is the complement of a prime ideal of R.

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

The localization of R at the complement of a prime ideal, as a quotient type.

Equations
@[instance]
def localization_map.at_prime.local_ring {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {I : ideal R} [hp : I.is_prime] (f : localization_map.at_prime S I) :

When f is a localization map from R at the complement of a prime ideal I, we use a copy of the localization map f's codomain S carrying the data of f so that the local_ring instance on S can 'know' the map needed to induce the instance.

@[instance]

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

theorem localization_map.mem_map_to_map_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {I : ideal R} {z : S} :
z ideal.map f.to_map I ∃ (x : I × M), z * (f.to_map) (x.snd) = (f.to_map) (x.fst)

theorem localization_map.map_comap {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (J : ideal S) :

theorem localization_map.comap_map_of_is_prime_disjoint {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (I : ideal R) :

def localization_map.order_embedding {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring 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 localization_map.is_prime_of_is_prime_disjoint {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (I : ideal R) :

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 localization_map.order_iso_of_prime {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring 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

Equations

algebra section

Defines the R-algebra instance on a copy of S carrying the data of the localization map f needed to induce the R-algebra structure.

@[instance]
def localization_map.algebra {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

We use a copy of the localization map f's codomain S carrying the data of f so that the R-algebra instance on S can 'know' the map needed to induce the R-algebra structure.

Equations
@[instance]
def localization.algebra {R : Type u_1} [comm_ring R] {M : submonoid R} :

Equations
@[simp]
theorem localization_map.of_id {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) (a : R) :

@[simp]
theorem localization_map.algebra_map_eq {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

def localization_map.lin_coe {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

Localization map f from R to S as an R-linear map.

Equations
def localization_map.coe_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

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

Equations
theorem localization_map.mem_coe_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (I : ideal R) {x : S} :
x f.coe_submodule I ∃ (y : R), y I (f.to_map) y = x

@[simp]
theorem localization_map.lin_coe_apply {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {x : R} :
(f.lin_coe) x = (f.to_map) x

theorem localization_map.map_smul {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {P : Type u_3} [comm_ring P] {f : localization_map M S} {g : R →+* P} {T : submonoid P} (hy : ∀ (y : M), g y T) {Q : Type u_4} [comm_ring Q] (k : localization_map T Q) (x : f.codomain) (z : R) :
(f.map hy k) (z x) = g z (f.map hy k) x

def localization.alg_equiv_of_quotient {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

Given a localization map f : R →+* S for a submonoid M, we get an R-preserving isomorphism between the localization of R at M as a quotient type and S.

Equations
def localization_map.coeff_integer_normalization {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} :
polynomial f.codomain → R

coeff_integer_normalization p gives the coefficients of the polynomial integer_normalization p

Equations
def localization_map.integer_normalization {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} :

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

Equations
theorem localization_map.integer_normalization_spec {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} (p : polynomial f.codomain) :
∃ (b : M), ∀ (i : ), (f.to_map) ((localization_map.integer_normalization p).coeff i) = ((f.to_map) b) * p.coeff i

theorem localization_map.integer_normalization_eval₂_eq_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {R' : Type u_4} [comm_ring R'] (g : f.codomain →+* R') (p : polynomial f.codomain) {x : R'} :

theorem localization_map.integer_normalization_aeval_eq_zero {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {f : localization_map M S} {R' : Type u_4} [comm_ring R'] [algebra R R'] [algebra f.codomain R'] [is_scalar_tower R f.codomain R'] (p : polynomial f.codomain) {x : R'} :

theorem localization_map.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) {x : R} :
M non_zero_divisors R((f.to_map) x = 0 x = 0)

theorem localization_map.injective {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] (f : localization_map M S) :

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

The image of P in the localization at P.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

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

def fraction_map (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] :
Type (max u_1 u_5)

Localization map from an integral domain R to its field of fractions.

Equations
theorem fraction_map.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] (φ : fraction_map R K) {x : R} :

theorem fraction_map.injective {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] (φ : fraction_map R K) :

def fraction_map.to_integral_domain {A : Type u_4} [integral_domain A] {K : Type u_5} [comm_ring K] :

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

Equations
def fraction_map.inv {A : Type u_4} [integral_domain A] {K : Type u_5} [comm_ring K] :
fraction_map A KK → K

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

Equations
theorem fraction_map.mul_inv_cancel {A : Type u_4} [integral_domain A] {K : Type u_5} [comm_ring K] (φ : fraction_map A K) (x : K) :
x 0x * φ.inv x = 1

def fraction_map.to_field {A : Type u_4} [integral_domain A] {K : Type u_5} [comm_ring K] :

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

Equations
theorem fraction_map.mk'_eq_div {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] (f : fraction_map A K) {r : A} {s : (non_zero_divisors A)} :

theorem fraction_map.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 fraction_map.lift {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] (f : fraction_map A K) {g : A →+* L} :

Given an integral domain A, a localization map to its fields of fractions f : A →+* 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 fraction_map.lift_mk' {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] (f : fraction_map A K) {g : A →+* L} (hg : function.injective g) (x : A) (y : (non_zero_divisors A)) :
(f.lift hg) (localization_map.mk' f x y) = g x / g y

Given an integral domain A, a localization map to its fields of fractions f : A →+* 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 fraction_map.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] (f : fraction_map A K) (g : fraction_map B L) {j : A →+* B} :

Given integral domains A, B and localization maps to their fields of fractions f : A →+* K, g : B →+* 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 fraction_map.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] :
fraction_map A Kfraction_map B LA ≃+* BK ≃+* 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

The cast from int to rat as a fraction_map.

Equations

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

theorem fraction_map.exists_reduced_fraction {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) (x : localization_map.codomain φ) :
∃ (a : A) (b : (non_zero_divisors A)), (∀ {d : A}, d ad bis_unit d) localization_map.mk' φ a b = x

def fraction_map.num {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) :

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

Equations

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

Equations
theorem fraction_map.num_denom_reduced {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) (x : localization_map.codomain φ) {d : A} :
d φ.num xd (φ.denom x)is_unit d

@[simp]
theorem fraction_map.mk'_num_denom {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) (x : localization_map.codomain φ) :
localization_map.mk' φ (φ.num x) (φ.denom x) = x

theorem fraction_map.num_mul_denom_eq_num_mul_denom_iff_eq {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) {x y : localization_map.codomain φ} :
(φ.num y) * (φ.denom x) = (φ.num x) * (φ.denom y) x = y

theorem fraction_map.eq_zero_of_num_eq_zero {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) {x : localization_map.codomain φ} :
φ.num x = 0x = 0

theorem fraction_map.is_unit_denom_of_num_eq_zero {A : Type u_4} [integral_domain A] {K : Type u_5} [field K] [unique_factorization_monoid A] (φ : fraction_map A K) {x : localization_map.codomain φ} :
φ.num x = 0is_unit (φ.denom x)

def localization_algebra {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R S] (M : submonoid R) :

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] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R S] (f : localization_map M Rₘ) (g : localization_map (algebra.algebra_map_submonoid S M) Sₘ) (r : R) (m : M) :
(algebra_map Rₘ Sₘ) (f.mk' r m) = g.mk' ((algebra_map R S) r) (algebra_map R S) m, _⟩

theorem localization_algebra_injective {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R S] (f : localization_map M Rₘ) (g : localization_map (algebra.algebra_map_submonoid S M) Sₘ) :

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

theorem is_integral_localization_at_leading_coeff {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R S] (f : localization_map M Rₘ) (g : localization_map (algebra.algebra_map_submonoid S M) Sₘ) {x : S} (p : polynomial R) :

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] {Rₘ : Type u_6} {Sₘ : Type u_7} [comm_ring Rₘ] [comm_ring Sₘ] [algebra R S] (f : localization_map M Rₘ) (g : localization_map (algebra.algebra_map_submonoid S M) 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

def integral_closure.fraction_map_of_algebraic {A : Type u_4} [integral_domain A] {L : Type u_6} [field L] [algebra A L] :
algebra.is_algebraic A L(∀ (x : A), (algebra_map A L) x = 0x = 0)fraction_map (integral_closure A L) L

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

Equations

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.

Equations
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

Natural hom sending x : A, A an integral domain, to the equivalence class of (x, 1) in the field of fractions of A.

Equations

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