# mathlib3documentation

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 #

• 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 #

• 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 #

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

@[reducible]
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, norm_cast]
theorem is_fraction_ring.coe_inj {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [ K] [ K] {a b : R} :
a = b a = b
@[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]  :
@[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 ) :
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, irreducible]
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
@[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] [ 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 ) :
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 : ) :
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 : , 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 : ) :
@[simp]
theorem is_fraction_ring.mk'_eq_zero_iff_eq_zero {R : Type u_1} [comm_ring R] {K : Type u_5} [field K] [ K] [ K] {x : R} {y : } :
y = 0 x = 0
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] [ K] [ K] {x : A} {y : } :
y = 1 x = y
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 : ) :
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_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] [ K] [ K] [comm_ring L] [ 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.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) :
@[protected]
theorem is_fraction_ring.nontrivial (R : Type u_1) (S : Type u_2) [comm_ring R] [nontrivial R] [comm_ring S] [ S] [ S] :
@[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
@[protected, instance]
def fraction_ring.unique (R : Type u_1) [comm_ring R] [subsingleton R] :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def fraction_ring.field {A : Type u_4} [comm_ring A] [is_domain A] :
Equations
@[simp]
theorem fraction_ring.mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {r : A} {s : } :
@[protected, instance]
noncomputable def fraction_ring.algebra (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [ K]  :
K
Equations
@[protected, instance]
def fraction_ring.is_scalar_tower (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [ K]  :
K
noncomputable def fraction_ring.alg_equiv (A : Type u_4) [comm_ring A] [is_domain A] (K : Type u_1) [field K] [ K] [ 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
@[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] [ A]  :