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 Mathlib/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_6) [CommSemiring R] (K : Type u_7) [CommSemiring K] [Algebra R K] : Prop

IsFractionRing R K states K is the ring of fractions of a commutative ring R.

Equations

• IsFractionRing R K = IsLocalization (nonZeroDivisors R) K

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

instance Rat.isFractionRing : IsFractionRing ℤ ℚ

The cast from Int to Rat as a FractionRing.

instance instIsLocalizationIntPosRat : IsLocalization (Submonoid.pos ℤ) ℚ

As a corollary, Rat is also a localization at only positive integers.

instance NNRat.isFractionRing : IsFractionRing ℕ ℚ≥0

NNRat is the ring of fractions of Nat.

theorem IsFractionRing.of_field (R : Type u_1) [CommRing R] (K : Type u_5) [Field K] [Algebra R K] [FaithfulSMul R K] (surj : ∀ (z : K), ∃ (x : R) (y : R), z = (algebraMap R K) x / (algebraMap R K) y) : IsFractionRing R K

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)

theorem IsFractionRing.nonZeroDivisors_eq_isUnit (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] : nonZeroDivisors K = IsUnit.submonoid K

noncomputable def IsFractionRing.algEquiv (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] (L : Type u_6) [CommRing L] [Algebra K L] [IsFractionRing K L] : K ≃ₐ[K] L

If L is a fraction ring of K which is a fraction ring of R, the K-algebra homomorphism from K to L is an isomorphism.

Equations

• IsFractionRing.algEquiv R K L = IsLocalization.atUnits K (nonZeroDivisors K) ⋯

theorem IsFractionRing.idem (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsFractionRing K K

theorem IsFractionRing.trans (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] (L : Type u_6) [CommRing L] [Algebra K L] [IsFractionRing K L] [Algebra R L] [IsScalarTower R K L] : IsFractionRing R L

Taking fraction ring is idempotent: a fraction ring of a fraction ring of R is itself a fraction ring of R.

@[instance 100]

instance IsFractionRing.instFaithfulSMul (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] : FaithfulSMul R K

theorem IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit {R : Type u_1} [CommRing R] : IsFractionRing R R ↔ nonZeroDivisors R = IsUnit.submonoid R

theorem IsFractionRing.self_iff_nonZeroDivisors_le_isUnit {R : Type u_1} [CommRing R] : IsFractionRing R R ↔ nonZeroDivisors R ≤ IsUnit.submonoid R

theorem IsFractionRing.self_iff_bijective {R : Type u_1} [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsFractionRing R R ↔ Function.Bijective ⇑(algebraMap R K)

theorem IsFractionRing.self_iff_surjective {R : Type u_1} [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsFractionRing R R ↔ Function.Surjective ⇑(algebraMap R K)

theorem IsFractionRing.coe_inj {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] {a b : R} : ↑a = ↑b ↔ a = b

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] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] [IsDomain A] : 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] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] [IsDomain A] (z : K) : K

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

Equations

• 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.inv_def (A : Type u_6) [CommRing A] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] [IsDomain A] (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] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] [IsDomain A] (x : K) (hx : x ≠ 0) : x * IsFractionRing.inv A x = 1

@[reducible, inline]

noncomputable abbrev IsFractionRing.toField (A : Type u_4) [CommRing A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] [IsDomain A] : 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

• One or more equations did not get rendered due to their size.

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] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {r 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] {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] {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] {L : Type u_7} [Field L] {g : A →+* L} (hg : Function.Injective ⇑g) (y : ↥(nonZeroDivisors A)) : IsUnit (g ↑y)

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] {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

theorem IsFractionRing.algHom_commutes {A : Type u_4} [CommRing A] {B : Type u_6} [CommRing B] [Algebra A B] {K₁ : Type u_8} {K₂ : Type u_9} [Field K₁] [Field K₂] [Algebra A K₁] [Algebra A K₂] [IsFractionRing A K₁] {L₁ : Type u_10} {L₂ : Type u_11} [Field L₁] [Field L₂] [Algebra B L₁] [Algebra B L₂] [Algebra K₁ L₁] [Algebra K₂ L₂] [Algebra A L₁] [Algebra A L₂] [IsScalarTower A K₁ L₁] [IsScalarTower A K₂ L₂] [IsScalarTower A B L₁] [IsScalarTower A B L₂] (e : K₁ →ₐ[A] K₂) (f : L₁ →ₐ[B] L₂) (x : K₁) : (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

theorem IsFractionRing.algEquiv_commutes {A : Type u_4} [CommRing A] {B : Type u_6} [CommRing B] [Algebra A B] {K₁ : Type u_8} {K₂ : Type u_9} [Field K₁] [Field K₂] [Algebra A K₁] [Algebra A K₂] [IsFractionRing A K₁] {L₁ : Type u_10} {L₂ : Type u_11} [Field L₁] [Field L₂] [Algebra B L₁] [Algebra B L₂] [Algebra K₁ L₁] [Algebra K₂ L₂] [Algebra A L₁] [Algebra A L₂] [IsScalarTower A K₁ L₁] [IsScalarTower A K₂ L₂] [IsScalarTower A B L₁] [IsScalarTower A B L₂] (e : K₁ ≃ₐ[A] K₂) (f : L₁ ≃ₐ[B] L₂) (x : K₁) : (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

theorem IsFractionRing.closure_range_algebraMap (A : Type u_4) [CommRing A] (K : Type u_5) [Field K] [Algebra A K] [IsFractionRing A K] : Subfield.closure (Set.range ⇑(algebraMap A K)) = ⊤

If A is a commutative ring with fraction field K, then the subfield of K generated by the image of algebraMap A K is equal to the whole field K.

theorem IsFractionRing.ringHom_fieldRange_eq_of_comp_eq {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_8} [Field L] {g : A →+* L} {f : K →+* L} (h : f.comp (algebraMap A K) = g) : f.fieldRange = Subfield.closure ↑g.range

If A is a commutative ring with fraction field K, L is a field, g : A →+* L lifts to f : K →+* L, then the image of f is the subfield generated by the image of g.

theorem IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_8} [Field L] {g : A →+* L} {f : K →+* L} (h : f.comp (algebraMap A K) = g) {s : Set L} (hs : g.range = Subring.closure s) : f.fieldRange = Subfield.closure s

If A is a commutative ring with fraction field K, L is a field, g : A →+* L lifts to f : K →+* L, s is a set such that the image of g is the subring generated by s, then the image of f is the subfield generated by s.

noncomputable def IsFractionRing.lift {A : Type u_4} [CommRing 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 a commutative ring 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 ⋯

theorem IsFractionRing.lift_unique {A : Type u_4} [CommRing 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) {f : K →+* L} (hf1 : ∀ (x : A), f ((algebraMap A K) x) = g x) : lift hg = f

theorem IsFractionRing.ringHom_ext {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {f1 f2 : K →+* L} (hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)) : f1 = f2

Another version of unique to give two lift maps should be equal

theorem IsFractionRing.injective_comp_algebraMap {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] : Function.Injective fun (f : K →+* L) => f.comp (algebraMap A K)

noncomputable def IsFractionRing.liftAlgHom {R : Type u_1} [CommRing R] {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] [Algebra R A] [Algebra R K] [IsScalarTower R A K] [Algebra R L] {g : A →ₐ[R] L} (hg : Function.Injective ⇑g) : K →ₐ[R] L

AlgHom version of IsFractionRing.lift.

Equations

• IsFractionRing.liftAlgHom hg = IsLocalization.liftAlgHom ⋯

theorem IsFractionRing.liftAlgHom_toRingHom {R : Type u_1} [CommRing R] {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] [Algebra R A] [Algebra R K] [IsScalarTower R A K] [Algebra R L] {g : A →ₐ[R] L} (hg : Function.Injective ⇑g) : (liftAlgHom hg).toRingHom = lift hg

@[simp]

theorem IsFractionRing.coe_liftAlgHom {R : Type u_1} [CommRing R] {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] [Algebra R A] [Algebra R K] [IsScalarTower R A K] [Algebra R L] {g : A →ₐ[R] L} (hg : Function.Injective ⇑g) : ⇑(liftAlgHom hg) = ⇑(lift hg)

theorem IsFractionRing.liftAlgHom_apply {R : Type u_1} [CommRing R] {A : Type u_4} [CommRing A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] [Algebra R A] [Algebra R K] [IsScalarTower R A K] [Algebra R L] {g : A →ₐ[R] L} (hg : Function.Injective ⇑g) (x : K) : (liftAlgHom hg) x = (lift hg) x

@[simp]

theorem IsFractionRing.lift_algebraMap {A : Type u_4} [CommRing 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) : (lift hg) ((algebraMap A K) x) = g x

Given a commutative ring 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_fieldRange {A : Type u_4} [CommRing 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) : (lift hg).fieldRange = Subfield.closure ↑g.range

The image of IsFractionRing.lift is the subfield generated by the image of the ring hom.

theorem IsFractionRing.lift_fieldRange_eq_of_range_eq {A : Type u_4} [CommRing 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) {s : Set L} (hs : g.range = Subring.closure s) : (lift hg).fieldRange = Subfield.closure s

The image of IsFractionRing.lift is the subfield generated by s, if the image of the ring hom is the subring generated by s.

theorem IsFractionRing.lift_mk' {A : Type u_4} [CommRing 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)) : (lift hg) (IsLocalization.mk' K x y) = g x / g ↑y

Given a commutative ring 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 commutative rings A, B where B is an integral domain, with fraction rings K, L and an injective ring hom j : A →+* B, we get a ring 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.ringEquivOfRingEquiv {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (h : A ≃+* B) : K ≃+* L

Given rings A, B and localization maps to their fraction rings f : A →+* K, g : B →+* L, an isomorphism h : A ≃+* B induces an isomorphism of fraction rings K ≃+* L.

Equations

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

@[simp]

theorem IsFractionRing.ringEquivOfRingEquiv_algebraMap {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (h : A ≃+* B) (a : A) : (ringEquivOfRingEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

@[simp]

theorem IsFractionRing.ringEquivOfRingEquiv_symm {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (h : A ≃+* B) : (ringEquivOfRingEquiv h).symm = ringEquivOfRingEquiv h.symm

noncomputable def IsFractionRing.algEquivOfAlgEquiv {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [CommSemiring R] [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra R A] [Algebra R K] [Algebra A K] [IsFractionRing A K] [IsScalarTower R A K] [Algebra R B] [Algebra R L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (h : A ≃ₐ[R] B) : K ≃ₐ[R] L

Given R-algebras A, B and localization maps to their fraction rings f : A →ₐ[R] K, g : B →ₐ[R] L, an isomorphism h : A ≃ₐ[R] B induces an isomorphism of fraction rings K ≃ₐ[R] L.

Equations

• IsFractionRing.algEquivOfAlgEquiv h = IsLocalization.algEquivOfAlgEquiv K L h ⋯

@[simp]

theorem IsFractionRing.algEquivOfAlgEquiv_algebraMap {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [CommSemiring R] [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra R A] [Algebra R K] [Algebra A K] [IsFractionRing A K] [IsScalarTower R A K] [Algebra R B] [Algebra R L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (h : A ≃ₐ[R] B) (a : A) : (algEquivOfAlgEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

@[simp]

theorem IsFractionRing.algEquivOfAlgEquiv_symm {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [CommSemiring R] [CommRing A] [CommRing B] [CommRing K] [CommRing L] [Algebra R A] [Algebra R K] [Algebra A K] [IsFractionRing A K] [IsScalarTower R A K] [Algebra R B] [Algebra R L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (h : A ≃ₐ[R] B) : (algEquivOfAlgEquiv h).symm = algEquivOfAlgEquiv h.symm

noncomputable def IsFractionRing.fieldEquivOfAlgEquiv {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing A] [CommRing B] [CommRing 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.ringEquivOfRingEquiv f.toRingEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing A] [CommRing B] [CommRing 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) : AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) = algEquivOfAlgEquiv f

@[simp]

theorem IsFractionRing.fieldEquivOfAlgEquiv_algebraMap {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing A] [CommRing B] [CommRing 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) : (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] [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] : 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] [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) : fieldEquivOfAlgEquiv FA FB FD (f.trans g) = (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g)

noncomputable def IsFractionRing.fieldEquivOfAlgEquivHom {A : Type u_8} {B : Type u_9} [CommRing A] [CommRing 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] [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) : (fieldEquivOfAlgEquivHom K L) f = fieldEquivOfAlgEquiv K L L f

theorem IsFractionRing.fieldEquivOfAlgEquivHom_injective (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing 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 ⇑(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_iff_nontrivial (R : Type u_8) (S : Type u_9) [CommSemiring R] [CommSemiring S] [Algebra R S] [h : IsFractionRing R S] : Nontrivial R ↔ Nontrivial S

theorem IsFractionRing.nontrivial (R : Type u_8) (S : Type u_9) [CommSemiring R] [CommSemiring S] [Algebra R S] [h : IsFractionRing R S] [hR : Nontrivial R] : 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 FaithfulSMul.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] : FaithfulSMul 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.instIsFractionRing (R : Type u_1) [CommRing R] : IsFractionRing (FractionRing R) (FractionRing R)

@[instance_reducible]

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)

@[instance_reducible]

noncomputable instance FractionRing.field (A : Type u_4) [CommRing A] [IsDomain A] : Field (FractionRing A)

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) [Field K] [Algebra R K] [FaithfulSMul 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) [Field K] [Algebra R K] [FaithfulSMul R K] : IsScalarTower R (FractionRing R) K

theorem FractionRing.algebraMap_liftAlgebra (R : Type u_1) [CommRing R] (K : Type u_5) [Field K] [Algebra R K] [FaithfulSMul R K] : have this := ⋯; algebraMap (FractionRing R) K = IsFractionRing.lift ⋯

instance FractionRing.instIsScalarTower (R : Type u_1) [CommRing R] (K : Type u_5) [Field K] [Algebra R K] [FaithfulSMul R K] {R₀ : Type u_6} [SMul R₀ R] [IsScalarTower R₀ R R] [SMul R₀ K] [IsScalarTower R₀ R K] : IsScalarTower R₀ (FractionRing R) K

noncomputable def FractionRing.algEquiv (A : Type u_4) [CommRing A] (K : Type u_6) [CommRing K] [Algebra A K] [IsFractionRing A K] : FractionRing A ≃ₐ[A] K

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

Equations

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

instance FractionRing.instFaithfulSMul (R : Type u_1) [CommRing R] (A : Type u_4) [CommRing A] [Algebra R A] [FaithfulSMul R A] : FaithfulSMul R (FractionRing A)

instance FractionRing.instIsScalarTower_1 (A : Type u_4) [CommRing A] [IsDomain A] (k : Type u_6) (K : Type u_7) [Field k] [Field K] [Algebra A k] [Algebra A K] [Algebra k K] [FaithfulSMul A k] [FaithfulSMul A K] [IsScalarTower A k K] : IsScalarTower (FractionRing A) k K