mathlib3 documentation

ring_theory.localization.fraction_ring

Fraction ring / fraction field Frac(R) as localization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Main results #

Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

Tags #

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

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

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

source
@[protected, instance]
def rat.is_fraction_ring  :
is_fraction_ring ℤ ℚ

The cast from int to rat as a fraction_ring.

source
theorem is_fraction_ring.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] {x : R} :
⇑(algebra_map R K) x = 0 ↔ x = 0
source
@[protected]
theorem is_fraction_ring.injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] [is_fraction_ring R K] :
function.injective ⇑(algebra_map R K)
source
@[simp, norm_cast]
theorem is_fraction_ring.coe_inj {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] {a b : R} :
↑a = ↑b ↔ a = b
source
@[protected, instance]
def is_fraction_ring.no_zero_smul_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] [no_zero_divisors K] :
no_zero_smul_divisors R K
source
@[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] [algebra R K] [is_fraction_ring R K] [nontrivial R] {x : R} (hx : x ∈ non_zero_divisors R) :
⇑(algebra_map R K) x ≠ 0
source
@[protected]
theorem is_fraction_ring.is_domain (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :
is_domain K

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

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

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

Equations
source
@[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] [algebra A K] [is_fraction_ring A K] (x : K) (hx : x ≠ 0) :
x * is_fraction_ring.inv A x = 1
source
@[reducible]
noncomputable def is_fraction_ring.to_field (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :
field 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
source
theorem is_fraction_ring.mk'_mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r s : A} (hs : s ∈ non_zero_divisors A) :
is_localization.mk' K r ⟨s, hs⟩ = ⇑(algebra_map A K) r / ⇑(algebra_map A K) s
source
@[simp]
theorem is_fraction_ring.mk'_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r : A} (s : ↥(non_zero_divisors A)) :
is_localization.mk' K r s = ⇑(algebra_map A K) r / ⇑(algebra_map A K) ↑s
source
theorem is_fraction_ring.div_surjective {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] (z : K) :
∃ (x y : A) (hy : y ∈ non_zero_divisors A), ⇑(algebra_map A K) x / ⇑(algebra_map A K) y = z
source
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 : ↥(non_zero_divisors A)) :
is_unit (⇑g ↑y)
source
@[simp]
theorem is_fraction_ring.mk'_eq_zero_iff_eq_zero {R : Type u_1} [comm_ring R] {K : Type u_5} [field K] [algebra R K] [is_fraction_ring R K] {x : R} {y : ↥(non_zero_divisors R)} :
is_localization.mk' K x y = 0 ↔ x = 0
source
theorem is_fraction_ring.mk'_eq_one_iff_eq {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {x : A} {y : ↥(non_zero_divisors A)} :
is_localization.mk' K x y = 1 ↔ x = ↑y
source
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] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective ⇑g) :
K →+* L

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

Equations
source
@[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] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective ⇑g) (x : A) :
⇑(is_fraction_ring.lift hg) (⇑(algebra_map 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.

source
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] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective ⇑g) (x : A) (y : ↥(non_zero_divisors A)) :
⇑(is_fraction_ring.lift hg) (is_localization.mk' K x 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.

source
noncomputable def is_fraction_ring.map {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} [comm_ring A] [comm_ring B] [is_domain B] [comm_ring K] [algebra A K] [is_fraction_ring A K] [comm_ring L] [algebra B L] [is_fraction_ring B L] {j : A →+* B} (hj : function.injective ⇑j) :
K →+* L

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

Equations
source
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] [algebra A K] [is_fraction_ring A K] [algebra B L] [is_fraction_ring B L] (h : A ≃+* B) :
K ≃+* L

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

Equations
source
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] [algebra R S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
is_fraction_ring R S ↔ is_fraction_ring P S
source
@[protected]
theorem is_fraction_ring.nontrivial (R : Type u_1) (S : Type u_2) [comm_ring R] [nontrivial R] [comm_ring S] [algebra R S] [is_fraction_ring R S] :
nontrivial S
source
@[reducible]
def fraction_ring (R : Type u_1) [comm_ring R] :
Type u_1

The fraction ring of a commutative ring R as a quotient type.

We instantiate this definition as generally as possible, and assume that the commutative ring R is an integral domain only when this is needed for proving.

Equations
source
@[protected, instance]
def fraction_ring.unique (R : Type u_1) [comm_ring R] [subsingleton R] :
unique (fraction_ring R)
Equations
source
@[protected, instance]
def fraction_ring.nontrivial (R : Type u_1) [comm_ring R] [nontrivial R] :
nontrivial (fraction_ring R)
source
@[protected, instance]
noncomputable def fraction_ring.field {A : Type u_4} [comm_ring A] [is_domain A] :
field (fraction_ring A)
Equations
source
@[simp]
theorem fraction_ring.mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {r : A} {s : ↥(non_zero_divisors A)} :
localization.mk r s = ⇑(algebra_map A (fraction_ring A)) r / ⇑(algebra_map A (fraction_ring A)) ↑s
source
@[protected, instance]
noncomputable def fraction_ring.algebra (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
algebra (fraction_ring R) K
Equations
source
@[protected, instance]
def fraction_ring.is_scalar_tower (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
is_scalar_tower R (fraction_ring R) K
source
noncomputable def fraction_ring.alg_equiv (A : Type u_4) [comm_ring A] [is_domain A] (K : Type u_1) [field K] [algebra A K] [is_fraction_ring A K] :
fraction_ring A ≃ₐ[A] K

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

Equations
source
@[protected, instance]
def fraction_ring.no_zero_smul_divisors (R : Type u_1) [comm_ring R] (A : Type u_4) [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :
no_zero_smul_divisors R (fraction_ring A)