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

## Main definitions #

• IsFractionRing R K expresses that K is a field of fractions of R, as an abbreviation of IsLocalization (NonZeroDivisors R) K

## Main results #

• IsFractionRing.field: a definition (not an instance) stating the localization of an integral domain R at R \ {0} is a field
• Rat.isFractionRing is an instance stating ℚ is the field of fractions of ℤ

## Implementation notes #

See RingTheory/Localization/Basic.lean for a design overview.

## Tags #

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

@[reducible, inline]
abbrev IsFractionRing (R : Type u_1) [] (K : Type u_5) [] [Algebra R K] :

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

Equations
Instances For
instance instIsFractionRing {R : Type u_6} [] :
Equations
• =

The cast from Int to Rat as a FractionRing.

Equations
theorem IsFractionRing.to_map_eq_zero_iff {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] {x : R} :
() x = 0 x = 0
theorem IsFractionRing.injective (R : Type u_1) [] (K : Type u_5) [] [Algebra R K] [] :
@[simp]
theorem IsFractionRing.coe_inj {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] {a : R} {b : R} :
a = b a = b
@[instance 100]
instance IsFractionRing.instNoZeroSMulDivisorsOfNoZeroDivisors {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] [] :
Equations
• =
theorem IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] [] {x : R} (hx : ) :
() x 0
theorem IsFractionRing.isDomain (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] :

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

@[irreducible]
noncomputable def IsFractionRing.inv (A : Type u_6) [] [] {K : Type u_7} [] [Algebra A K] [] (z : K) :
K

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

Equations
Instances For
theorem IsFractionRing.inv_def (A : Type u_6) [] [] {K : Type u_7} [] [Algebra A K] [] (z : K) :
= if h : z = 0 then 0 else IsLocalization.mk' K ().2 ().1,
theorem IsFractionRing.mul_inv_cancel (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] (x : K) (hx : x 0) :
x * = 1
@[reducible, inline]
noncomputable abbrev IsFractionRing.toField (A : Type u_4) [] [] {K : Type u_5} [] [Algebra A K] [] :

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

Equations
• = let __spread.0 := ; Field.mk zpowRec (fun (q : ℚ≥0) (a : K) => q * a) (fun (a : ) (x : K) => a * x)
Instances For
theorem IsFractionRing.surjective_iff_isField {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] [] :
theorem IsFractionRing.mk'_mk_eq_div {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {r : A} {s : A} (hs : ) :
IsLocalization.mk' K r s, hs = () r / () s
@[simp]
theorem IsFractionRing.mk'_eq_div {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {r : A} (s : ()) :
= () r / () s
theorem IsFractionRing.div_surjective {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] (z : K) :
∃ (x : A), y, () x / () y = z
theorem IsFractionRing.isUnit_map_of_injective {A : Type u_4} [] [] {L : Type u_7} [] {g : A →+* L} (hg : ) (y : ()) :
IsUnit (g y)
@[simp]
theorem IsFractionRing.mk'_eq_zero_iff_eq_zero {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] {x : R} {y : ()} :
= 0 x = 0
theorem IsFractionRing.mk'_eq_one_iff_eq {A : Type u_4} [] [] {K : Type u_5} [] [Algebra A K] [] {x : A} {y : ()} :
= 1 x = y
noncomputable def IsFractionRing.lift {A : Type u_4} [] [] {K : Type u_5} [] {L : Type u_7} [] [Algebra A K] [] {g : A →+* L} (hg : ) :
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 × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

Equations
Instances For
@[simp]
theorem IsFractionRing.lift_algebraMap {A : Type u_4} [] [] {K : Type u_5} [] {L : Type u_7} [] [Algebra A K] [] {g : A →+* L} (hg : ) (x : A) :
() (() 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 IsFractionRing.lift_mk' {A : Type u_4} [] [] {K : Type u_5} [] {L : Type u_7} [] [Algebra A K] [] {g : A →+* L} (hg : ) (x : 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 ∈ NonZeroDivisors A.

noncomputable def IsFractionRing.map {A : Type u_8} {B : Type u_9} {K : Type u_10} {L : Type u_11} [] [] [] [] [Algebra A K] [] [] [Algebra B L] [] {j : A →+* B} (hj : ) :
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 × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

Equations
Instances For
noncomputable def IsFractionRing.fieldEquivOfRingEquiv {A : Type u_4} [] [] {K : Type u_5} {B : Type u_6} [] [] [] {L : Type u_7} [] [Algebra A K] [] [Algebra 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
Instances For
theorem IsFractionRing.isFractionRing_iff_of_base_ringEquiv {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] (h : R ≃+* P) :
theorem IsFractionRing.nontrivial (R : Type u_8) (S : Type u_9) [] [] [] [Algebra R S] [] :
@[reducible, inline]
abbrev FractionRing (R : Type u_1) [] :
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.

In this generality, this construction is also known as the total fraction ring of R.

Equations
Instances For
instance FractionRing.unique (R : Type u_1) [] [] :
Equations
• = Localization.instUniqueLocalization
instance FractionRing.instNontrivial (R : Type u_1) [] [] :
Equations
• =
noncomputable instance FractionRing.field (A : Type u_4) [] [] :

Porting note: if the fields of this instance are explicitly defined as they were in mathlib3, the last instance in this file suffers a TC timeout

Equations
@[simp]
theorem FractionRing.mk_eq_div (A : Type u_4) [] [] {r : A} {s : ()} :
= () r / () s
@[reducible, inline]
noncomputable abbrev FractionRing.liftAlgebra (R : Type u_1) [] (K : Type u_5) [] [] [Algebra R K] [] :
Algebra () K

This is not an instance because it creates a diamond when K = FractionRing R. Should usually be introduced locally along with isScalarTower_liftAlgebra See note [reducible non-instances].

Equations
• = .toAlgebra
Instances For
instance FractionRing.isScalarTower_liftAlgebra (R : Type u_1) [] (K : Type u_5) [] [] [Algebra R K] [] :
Equations
• =
noncomputable def FractionRing.algEquiv (A : Type u_4) [] [] (K : Type u_6) [] [Algebra 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
Instances For
instance FractionRing.instNoZeroSMulDivisors (R : Type u_1) [] (A : Type u_4) [] [] [Algebra R A] [] :
Equations
• =