Documentation

Mathlib.RingTheory.Localization.FractionRing

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

Main definitions #

Main results #

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

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

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

Equations
source
instance instIsFractionRing {R : Type u_6} [Field R] :
IsFractionRing R R
Equations
  • ⋯ = ⋯
source
instance Rat.isFractionRing :
IsFractionRing ℤ ℚ

The cast from Int to Rat as a FractionRing.

Equations
source
theorem IsFractionRing.to_map_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] {x : R} :
(algebraMap R K) x = 0 ↔ x = 0
source
theorem IsFractionRing.injective (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] :
Function.Injective ⇑(algebraMap R K)
source
@[simp]
theorem IsFractionRing.coe_inj {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] {a : R} {b : R} :
↑a = ↑b ↔ a = b
source
@[instance 100]
instance IsFractionRing.instNoZeroSMulDivisorsOfNoZeroDivisors {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] [NoZeroDivisors K] :
NoZeroSMulDivisors R K
Equations
  • ⋯ = ⋯
source
theorem IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] {x : R} (hx : x ∈ nonZeroDivisors R) :
(algebraMap R K) x ≠ 0
source
theorem IsFractionRing.isDomain (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDomain K

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

source
theorem IsFractionRing.inv_def (A : Type u_6) [CommRing A] [IsDomain A] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] (z : K) :
IsFractionRing.inv A z = if h : z = 0 then 0 else IsLocalization.mk' K ↑(IsLocalization.sec (nonZeroDivisors A) z).2 ⟨(IsLocalization.sec (nonZeroDivisors A) z).1, ⋯⟩
source
@[irreducible]
noncomputable def IsFractionRing.inv (A : Type u_6) [CommRing A] [IsDomain A] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] (z : K) :
K

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

Equations
source
theorem IsFractionRing.mul_inv_cancel (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x ≠ 0) :
x * IsFractionRing.inv A x = 1
source
@[reducible, inline]
noncomputable abbrev IsFractionRing.toField (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] :
Field 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
source
theorem IsFractionRing.surjective_iff_isField {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] [IsDomain R] :
Function.Surjective ⇑(algebraMap R K) ↔ IsField R
source
theorem IsFractionRing.mk'_mk_eq_div {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {r : A} {s : A} (hs : s ∈ nonZeroDivisors A) :
IsLocalization.mk' K r ⟨s, hs⟩ = (algebraMap A K) r / (algebraMap A K) s
source
@[simp]
theorem IsFractionRing.mk'_eq_div {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {r : A} (s : ↥(nonZeroDivisors A)) :
IsLocalization.mk' K r s = (algebraMap A K) r / (algebraMap A K) ↑s
source
theorem IsFractionRing.div_surjective {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (z : K) :
∃ (x : A), ∃ y ∈ nonZeroDivisors A, (algebraMap A K) x / (algebraMap A K) y = z
source
theorem IsFractionRing.isUnit_map_of_injective {A : Type u_4} [CommRing A] [IsDomain A] {L : Type u_7} [Field L] {g : A →+* L} (hg : Function.Injective ⇑g) (y : ↥(nonZeroDivisors A)) :
IsUnit (g ↑y)
source
@[simp]
theorem IsFractionRing.mk'_eq_zero_iff_eq_zero {R : Type u_1} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {x : R} {y : ↥(nonZeroDivisors R)} :
IsLocalization.mk' K x y = 0 ↔ x = 0
source
theorem IsFractionRing.mk'_eq_one_iff_eq {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {x : A} {y : ↥(nonZeroDivisors A)} :
IsLocalization.mk' K x y = 1 ↔ x = ↑y
source
noncomputable def IsFractionRing.lift {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing 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 × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

Equations
source
@[simp]
theorem IsFractionRing.lift_algebraMap {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) (x : A) :
(IsFractionRing.lift hg) ((algebraMap 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 IsFractionRing.lift_mk' {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) (x : A) (y : ↥(nonZeroDivisors A)) :
(IsFractionRing.lift hg) (IsLocalization.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 ∈ NonZeroDivisors A.

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

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

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

Equations
source
instance FractionRing.unique (R : Type u_1) [CommRing R] [Subsingleton R] :
Unique (FractionRing R)
Equations
source
instance FractionRing.instNontrivial (R : Type u_1) [CommRing R] [Nontrivial R] :
Nontrivial (FractionRing R)
Equations
  • ⋯ = ⋯
source
noncomputable instance FractionRing.field (A : Type u_4) [CommRing A] [IsDomain A] :
Field (FractionRing A)

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
source
@[simp]
theorem FractionRing.mk_eq_div (A : Type u_4) [CommRing A] [IsDomain A] {r : A} {s : ↥(nonZeroDivisors A)} :
Localization.mk r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s
source
@[reducible, inline]
noncomputable abbrev FractionRing.liftAlgebra (R : Type u_1) [CommRing R] (K : Type u_5) [IsDomain R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :
Algebra (FractionRing R) 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
source
instance FractionRing.isScalarTower_liftAlgebra (R : Type u_1) [CommRing R] (K : Type u_5) [IsDomain R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :
IsScalarTower R (FractionRing R) K
Equations
  • ⋯ = ⋯
source
noncomputable def FractionRing.algEquiv (A : Type u_4) [CommRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] :
FractionRing 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
instance FractionRing.instNoZeroSMulDivisors (R : Type u_1) [CommRing R] (A : Type u_4) [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :
NoZeroSMulDivisors R (FractionRing A)
Equations
  • ⋯ = ⋯