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) [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

• IsFractionRing R K = IsLocalization (nonZeroDivisors R) K

instance instIsFractionRing {R : Type u_6} [Field R] : IsFractionRing R R

Equations

• ⋯ = ⋯

instance Rat.isFractionRing : IsFractionRing ℤ ℚ

The cast from Int to Rat as a FractionRing.

Equations

• Rat.isFractionRing = ⋯

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

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)

@[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

@[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

• ⋯ = ⋯

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

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.

@[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

• IsFractionRing.inv = IsFractionRing.wrapped✝.1

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, ⋯⟩

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

@[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

• IsFractionRing.toField A = Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

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

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

@[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

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

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)

@[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

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

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

• IsFractionRing.lift hg = IsLocalization.lift ⋯

@[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.

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.

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

• IsFractionRing.map hj = IsLocalization.map L j ⋯

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

• IsFractionRing.fieldEquivOfRingEquiv h = IsLocalization.ringEquivOfRingEquiv K L h ⋯

@[simp]

theorem IsFractionRing.fieldEquivOfRingEquiv_algebraMap {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) (a : A) : (IsFractionRing.fieldEquivOfRingEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

noncomputable def IsFractionRing.fieldEquivOfAlgEquiv {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing A] [CommRing B] [CommRing C] [IsDomain A] [IsDomain B] [IsDomain C] [Algebra A B] [Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [Field FA] [Field FB] [Field FC] [Algebra A FA] [Algebra B FB] [Algebra C FC] [IsFractionRing A FA] [IsFractionRing B FB] [IsFractionRing C FC] [Algebra A FB] [IsScalarTower A B FB] [Algebra A FC] [IsScalarTower A C FC] [Algebra FA FB] [IsScalarTower A FA FB] [Algebra FA FC] [IsScalarTower A FA FC] (f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC

An algebra isomorphism of rings induces an algebra isomorphism of fraction fields.

Equations

• IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f = { toEquiv := (IsFractionRing.fieldEquivOfRingEquiv f.toRingEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem IsFractionRing.fieldEquivOfAlgEquiv_algebraMap {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing A] [CommRing B] [CommRing C] [IsDomain A] [IsDomain B] [IsDomain C] [Algebra A B] [Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [Field FA] [Field FB] [Field FC] [Algebra A FA] [Algebra B FB] [Algebra C FC] [IsFractionRing A FA] [IsFractionRing B FB] [IsFractionRing C FC] [Algebra A FB] [IsScalarTower A B FB] [Algebra A FC] [IsScalarTower A C FC] [Algebra FA FB] [IsScalarTower A FA FB] [Algebra FA FC] [IsScalarTower A FA FC] (f : B ≃ₐ[A] C) (b : B) : (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f) ((algebraMap B FB) b) = (algebraMap C FC) (f b)

This says that fieldEquivOfAlgEquiv f is an extension of f (i.e., it agrees with f on B). Whereas (fieldEquivOfAlgEquiv f).commutes says that fieldEquivOfAlgEquiv f fixes K.

@[simp]

theorem IsFractionRing.fieldEquivOfAlgEquiv_refl (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra A B] (FA : Type u_12) (FB : Type u_13) [Field FA] [Field FB] [Algebra A FA] [Algebra B FB] [IsFractionRing A FA] [IsFractionRing B FB] [Algebra A FB] [IsScalarTower A B FB] [Algebra FA FB] [IsScalarTower A FA FB] : IsFractionRing.fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl = AlgEquiv.refl

theorem IsFractionRing.fieldEquivOfAlgEquiv_trans {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} [CommRing A] [CommRing B] [CommRing C] [CommRing D] [IsDomain A] [IsDomain B] [IsDomain C] [IsDomain D] [Algebra A B] [Algebra A C] [Algebra A D] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) (FD : Type u_15) [Field FA] [Field FB] [Field FC] [Field FD] [Algebra A FA] [Algebra B FB] [Algebra C FC] [Algebra D FD] [IsFractionRing A FA] [IsFractionRing B FB] [IsFractionRing C FC] [IsFractionRing D FD] [Algebra A FB] [IsScalarTower A B FB] [Algebra A FC] [IsScalarTower A C FC] [Algebra A FD] [IsScalarTower A D FD] [Algebra FA FB] [IsScalarTower A FA FB] [Algebra FA FC] [IsScalarTower A FA FC] [Algebra FA FD] [IsScalarTower A FA FD] (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) : IsFractionRing.fieldEquivOfAlgEquiv FA FB FD (f.trans g) = (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f).trans (IsFractionRing.fieldEquivOfAlgEquiv FA FC FD g)

noncomputable def IsFractionRing.fieldEquivOfAlgEquivHom {A : Type u_8} {B : Type u_9} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra A B] (K : Type u_10) (L : Type u_11) [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [Algebra K L] [IsScalarTower A K L] : (B ≃ₐ[A] B) →* L ≃ₐ[K] L

An algebra automorphism of a ring induces an algebra automorphism of its fraction field.

This is a bundled version of fieldEquivOfAlgEquiv.

Equations

• IsFractionRing.fieldEquivOfAlgEquivHom K L = { toFun := IsFractionRing.fieldEquivOfAlgEquiv K L L, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem IsFractionRing.fieldEquivOfAlgEquivHom_apply {A : Type u_8} {B : Type u_9} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra A B] (K : Type u_10) (L : Type u_11) [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [Algebra K L] [IsScalarTower A K L] (f : B ≃ₐ[A] B) : (IsFractionRing.fieldEquivOfAlgEquivHom K L) f = IsFractionRing.fieldEquivOfAlgEquiv K L L f

theorem IsFractionRing.fieldEquivOfAlgEquivHom_injective (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra A B] (K : Type u_10) (L : Type u_11) [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [Algebra K L] [IsScalarTower A K L] : Function.Injective ⇑(IsFractionRing.fieldEquivOfAlgEquivHom K L)

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

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

theorem algebraMap_injective_of_field_isFractionRing (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (K : Type u_6) (L : Type u_7) [Field K] [Semiring L] [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : Function.Injective ⇑(algebraMap R S)

theorem NoZeroSMulDivisors.of_field_isFractionRing (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] [NoZeroDivisors S] (K : Type u_6) (L : Type u_7) [Field K] [Semiring L] [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : NoZeroSMulDivisors R S

@[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

• FractionRing R = Localization (nonZeroDivisors R)

instance FractionRing.unique (R : Type u_1) [CommRing R] [Subsingleton R] : Unique (FractionRing R)

Equations

• FractionRing.unique R = inferInstance

instance FractionRing.instNontrivial (R : Type u_1) [CommRing R] [Nontrivial R] : Nontrivial (FractionRing R)

Equations

• ⋯ = ⋯

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

• FractionRing.field A = inferInstance

@[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

@[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

• FractionRing.liftAlgebra R K = (IsFractionRing.lift ⋯).toAlgebra

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

• ⋯ = ⋯

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

• FractionRing.algEquiv A K = Localization.algEquiv (nonZeroDivisors A) K

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

• ⋯ = ⋯