Fraction fields of localizations, polynomial rings and finite extensions

Main results

• IsFractionRing.liftOfLocalization: a nonzero localization of a domain embeds compatibly in any fraction field of the domain, which is then a fraction field of the localization (IsFractionRing.isFractionRing_liftOfLocalization).
• MvPolynomial.coeffFractionRingEmbedding: a fraction field of a coefficient domain A embeds canonically in a fraction field of MvPolynomial σ A, compatibly with A and its ground field.
• MvPolynomial.fractionRingCoeffMap, MvPolynomial.isFractionRing_fractionRingCoeffMap: enlarging the coefficients to their fraction field does not change the fraction field of a polynomial ring.
• IsFractionRing.exists_ne_zero_mul_mem_range_of_finite: a finite extension of domains with a common fraction field has a nonzero conductor element.

theorem IsLocalization.submonoid_coe_ne_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] (y : ↥M) : ↑y ≠ 0

The elements of the submonoid of a nontrivial localization are nonzero.

noncomputable def IsFractionRing.liftOfLocalization {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommRing R] [CommRing S] [Nontrivial S] [Field F] [Algebra R S] [Algebra R F] (M : Submonoid R) [IsLocalization M S] [IsFractionRing R F] : S →+* F

A localization of a domain embeds compatibly in any fraction field of the domain.

Equations

• IsFractionRing.liftOfLocalization M = IsLocalization.lift ⋯

theorem IsFractionRing.liftOfLocalization_comp {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommRing R] [CommRing S] [Nontrivial S] [Field F] [Algebra R S] [Algebra R F] (M : Submonoid R) [IsLocalization M S] [IsFractionRing R F] : (liftOfLocalization M).comp (algebraMap R S) = algebraMap R F

The embedding liftOfLocalization M of the localization S into a fraction field F of R restricts to the algebra map R → F along R → S.

theorem IsFractionRing.isFractionRing_liftOfLocalization {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommRing R] [IsDomain R] [CommRing S] [Nontrivial S] [Field F] [Algebra R S] [Algebra R F] (M : Submonoid R) [IsLocalization M S] [IsFractionRing R F] : have this := (liftOfLocalization M).toAlgebra; IsFractionRing S F

A fraction field of a domain is a fraction field of each of its nonzero localizations.

theorem MvPolynomial.algebraMap_injective_of_isFractionRing {A : Type u_1} {E : Type u_2} {σ : Type u_3} [CommRing A] [Field E] [Algebra A E] [Algebra (MvPolynomial σ A) E] [IsScalarTower A (MvPolynomial σ A) E] [IsFractionRing (MvPolynomial σ A) E] : Function.Injective ⇑(algebraMap A E)

The coefficients embed in a fraction field of a polynomial ring over a domain.

noncomputable def MvPolynomial.coeffFractionRingEmbedding {K : Type u_1} {A : Type u_2} {F : Type u_3} {E : Type u_4} {σ : Type u_5} [Field K] [CommRing A] [Field F] [Field E] [Algebra K A] [Algebra K F] [Algebra K E] [Algebra A F] [IsFractionRing A F] [IsScalarTower K A F] [Algebra A E] [IsScalarTower K A E] [Algebra (MvPolynomial σ A) E] [IsScalarTower A (MvPolynomial σ A) E] [IsFractionRing (MvPolynomial σ A) E] : F →ₐ[K] E

The embedding of a fraction field of the coefficients into a fraction field of the polynomial ring.

Equations

• MvPolynomial.coeffFractionRingEmbedding = IsFractionRing.liftAlgHom ⋯

theorem MvPolynomial.coeffFractionRingEmbedding_algebraMap {K : Type u_1} {A : Type u_2} {F : Type u_3} {E : Type u_4} {σ : Type u_5} [Field K] [CommRing A] [Field F] [Field E] [Algebra K A] [Algebra K F] [Algebra K E] [Algebra A F] [IsFractionRing A F] [IsScalarTower K A F] [Algebra A E] [IsScalarTower K A E] [Algebra (MvPolynomial σ A) E] [IsScalarTower A (MvPolynomial σ A) E] [IsFractionRing (MvPolynomial σ A) E] (x : A) : coeffFractionRingEmbedding ((algebraMap A F) x) = (algebraMap A E) x

The embedding coeffFractionRingEmbedding of a fraction field F of A into E sends the image of x : A in F to the image of x in E.

theorem MvPolynomial.isScalarTower_coeffFractionRingEmbedding {K : Type u_1} {A : Type u_2} {F : Type u_3} {E : Type u_4} {σ : Type u_5} [Field K] [CommRing A] [Field F] [Field E] [Algebra K A] [Algebra K F] [Algebra K E] [Algebra A F] [IsFractionRing A F] [IsScalarTower K A F] [Algebra A E] [IsScalarTower K A E] [Algebra (MvPolynomial σ A) E] [IsScalarTower A (MvPolynomial σ A) E] [IsFractionRing (MvPolynomial σ A) E] : have this := coeffFractionRingEmbedding.toAlgebra; IsScalarTower A F E

With the F-algebra structure on E given by coeffFractionRingEmbedding, the rings A, F and E form a scalar tower.

noncomputable def MvPolynomial.fractionRingCoeffMap {A : Type u_1} {K : Type u_2} {F : Type u_3} {σ : Type u_4} [CommRing A] [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ A) F] : MvPolynomial σ K →+* F

Extend polynomial coefficients inside the ambient fraction field.

Equations

• MvPolynomial.fractionRingCoeffMap = MvPolynomial.eval₂Hom (algebraMap K F) fun (i : σ) => (algebraMap (MvPolynomial σ A) F) (MvPolynomial.X i)

theorem MvPolynomial.fractionRingCoeffMap_comp {A : Type u_1} {K : Type u_2} {F : Type u_3} {σ : Type u_4} [CommRing A] [Field K] [Field F] [Algebra A K] [Algebra A F] [Algebra K F] [IsScalarTower A K F] [Algebra (MvPolynomial σ A) F] [IsScalarTower A (MvPolynomial σ A) F] : fractionRingCoeffMap.comp (map (algebraMap A K)) = algebraMap (MvPolynomial σ A) F

Composing fractionRingCoeffMap with the coefficient map MvPolynomial σ A → MvPolynomial σ K gives the algebra map MvPolynomial σ A → F.

theorem MvPolynomial.isFractionRing_fractionRingCoeffMap {A : Type u_1} {K : Type u_2} {F : Type u_3} {σ : Type u_4} [CommRing A] [IsDomain A] [Field K] [Field F] [Algebra A K] [IsFractionRing A K] [Algebra A F] [Algebra K F] [IsScalarTower A K F] [Algebra (MvPolynomial σ A) F] [IsScalarTower A (MvPolynomial σ A) F] [IsFractionRing (MvPolynomial σ A) F] : have this := fractionRingCoeffMap.toAlgebra; IsFractionRing (MvPolynomial σ K) F

The constructed coefficient extension realizes the same ambient field as a fraction field after coefficient localization.

theorem IsFractionRing.exists_ne_zero_mul_mem_range_of_finite (R : Type u_1) (A : Type u_2) (F : Type u_3) [CommRing R] [IsDomain R] [CommRing A] [Field F] [Algebra R A] [Algebra R F] [Algebra A F] [IsScalarTower R A F] [IsFractionRing R F] [IsFractionRing A F] [Module.Finite R A] : ∃ (c : R), c ≠ 0 ∧ ∀ (a : A), ∃ (r : R), (algebraMap R A) r = (algebraMap R A) c * a

A common nonzero denominator for a finite birational extension.