# Integral and algebraic elements of a fraction field #

## 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

source
noncomputable def IsLocalization.coeffIntegerNormalization {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) (i : ℕ) :
R

`coeffIntegerNormalization p` gives the coefficients of the polynomial `integerNormalization p`

Equations

- IsLocalization.coeffIntegerNormalization M p i = if hi : i ∈ p.support then Classical.choose ⋯ else 0

Instances For

source
theorem IsLocalization.coeffIntegerNormalization_of_coeff_zero {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) (i : ℕ) (h : p.coeff i = 0) :
coeffIntegerNormalization M p i = 0
source
@[deprecated IsLocalization.coeffIntegerNormalization_of_coeff_zero (since := "2025-05-23")]
theorem IsLocalization.coeffIntegerNormalization_of_not_mem_support {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) (i : ℕ) (h : p.coeff i = 0) :
coeffIntegerNormalization M p i = 0

Alias of `IsLocalization.coeffIntegerNormalization_of_coeff_zero`.

source
theorem IsLocalization.coeffIntegerNormalization_mem_support {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) (i : ℕ) (h : coeffIntegerNormalization M p i ≠ 0) :
i ∈ p.support
source
noncomputable def IsLocalization.integerNormalization {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) :
Polynomial R

`integerNormalization g` normalizes `g` to have integer coefficients by clearing the denominators

Equations

- IsLocalization.integerNormalization M p = ∑ i ∈ p.support, (Polynomial.monomial i) (IsLocalization.coeffIntegerNormalization M p i)

Instances For

source
@[simp]
theorem IsLocalization.integerNormalization_coeff {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) (i : ℕ) :
(integerNormalization M p).coeff i = coeffIntegerNormalization M p i
source
theorem IsLocalization.integerNormalization_spec {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) :
∃ (b : ↥M), ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
source
theorem IsLocalization.integerNormalization_map_to_map {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) :
∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
source
theorem IsLocalization.integerNormalization_eval₂_eq_zero {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] {R' : Type u_3} [CommRing R'] (g : S →+* R') (p : Polynomial S) {x : R'} (hx : Polynomial.eval₂ g x p = 0) :
Polynomial.eval₂ (g.comp (algebraMap R S)) x (integerNormalization M p) = 0
source
theorem IsLocalization.integerNormalization_aeval_eq_zero {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] {R' : Type u_3} [CommRing R'] [Algebra R R'] [Algebra S R'] [IsScalarTower R S R'] (p : Polynomial S) {x : R'} (hx : (Polynomial.aeval x) p = 0) :
(Polynomial.aeval x) (integerNormalization M p) = 0
source
theorem IsFractionRing.integerNormalization_eq_zero_iff {A : Type u_3} {K : Type u_4} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial K} :
IsLocalization.integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
source
theorem IsFractionRing.isAlgebraic_iff (A : Type u_3) (K : Type u_4) (C : Type u_5) [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing C] [Algebra A C] [Algebra K C] [IsScalarTower A K C] {x : C} :
IsAlgebraic A x ↔ IsAlgebraic K x

An element of a ring is algebraic over the ring `A` iff it is algebraic over the field of fractions of `A`.

source
theorem IsFractionRing.comap_isAlgebraic_iff {A : Type u_3} {K : Type u_4} {C : Type u_5} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing C] [Algebra A C] [Algebra K C] [IsScalarTower A K C] :
Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C

A ring is algebraic over the ring `A` iff it is algebraic over the field of fractions of `A`.

source
theorem RingHom.isIntegralElem_localization_at_leadingCoeff {R : Type u_5} {S : Type u_6} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hf : Polynomial.eval₂ f x p = 0) (M : Submonoid R) (hM : p.leadingCoeff ∈ M) {Rₘ : Type u_7} {Sₘ : Type u_8} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Submonoid.map f M) Sₘ] :
(IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
source
theorem is_integral_localization_at_leadingCoeff {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {x : S} (p : Polynomial R) (hp : (Polynomial.aeval x) p = 0) (hM : p.leadingCoeff ∈ M) :
(IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)

Given a particular witness to an element being algebraic over an algebra `R → S`, We can localize to a submonoid containing the leading coefficient to make it integral. Explicitly, the map between the localizations will be an integral ring morphism

source
theorem isIntegral_localization {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra.IsIntegral R S] :
(IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral

If `R → S` is an integral extension, `M` is a submonoid of `R`, `Rₘ` is the localization of `R` at `M`, and `Sₘ` is the localization of `S` at the image of `M` under the extension map, then the induced map `Rₘ → Sₘ` is also an integral extension

source
theorem isIntegral_localization' {R : Type u_5} {S : Type u_6} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsIntegral) (M : Submonoid R) :
(IsLocalization.map (Localization (Submonoid.map (↑f) M)) f ⋯).IsIntegral
source
theorem IsLocalization.scaleRoots_commonDenom_mem_lifts {R : Type u_1} [CommRing R] (M : Submonoid R) {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] (p : Polynomial Rₘ) (hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range) :
p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∈ Polynomial.lifts (algebraMap R Rₘ)
source
theorem IsIntegral.exists_multiple_integral_of_isLocalization {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra Rₘ S] [IsScalarTower R Rₘ S] (x : S) (hx : IsIntegral Rₘ x) :
∃ (m : ↥M), IsIntegral R (m • x)
source
theorem IsIntegralClosure.isFractionRing_of_algebraic (A : Type u_3) [CommRing A] {L : Type u_5} [Field L] [Algebra A L] (C : Type u_6) [CommRing C] [IsDomain C] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [Algebra.IsAlgebraic A L] (inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0) :
IsFractionRing C L

If the field `L` is an algebraic extension of the integral domain `A`, the integral closure `C` of `A` in `L` has fraction field `L`.

source
theorem IsIntegralClosure.isFractionRing_of_finite_extension (A : Type u_3) (K : Type u_4) [CommRing A] (L : Type u_5) [Field K] [Field L] [Algebra A K] [Algebra A L] [IsFractionRing A K] (C : Type u_6) [CommRing C] [IsDomain C] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [IsDomain A] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] :
IsFractionRing C L

If the field `L` is a finite extension of the fraction field of the integral domain `A`, the integral closure `C` of `A` in `L` has fraction field `L`.

source
theorem integralClosure.isFractionRing_of_algebraic {A : Type u_3} [CommRing A] {L : Type u_5} [Field L] [Algebra A L] [Algebra.IsAlgebraic A L] (inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0) :
IsFractionRing (↥(integralClosure A L)) L

If the field `L` is an algebraic extension of the integral domain `A`, the integral closure of `A` in `L` has fraction field `L`.

source
theorem integralClosure.isFractionRing_of_finite_extension {A : Type u_3} (K : Type u_4) [CommRing A] (L : Type u_5) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [IsDomain A] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] :
IsFractionRing (↥(integralClosure A L)) L

If the field `L` is a finite extension of the fraction field of the integral domain `A`, the integral closure of `A` in `L` has fraction field `L`.

source
theorem IsFractionRing.isAlgebraic_iff' (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (K : Type u_4) [Field K] [IsDomain R] [Algebra R K] [Algebra S K] [NoZeroSMulDivisors R K] [IsFractionRing S K] [IsScalarTower R S K] :
Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K

`S` is algebraic over `R` iff a fraction ring of `S` is algebraic over `R`

source
theorem IsFractionRing.ideal_span_singleton_map_subset (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {K : Type u_4} {L : Type u_5} [IsDomain R] [IsDomain S] [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra S L] [Algebra.IsAlgebraic R S] [IsFractionRing S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] {a : S} {b : Set S} (inj : Function.Injective ⇑(algebraMap R L)) (h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)) :
↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

If the `S`-multiples of `a` are contained in some `R`-span, then `Frac(S)`-multiples of `a` are contained in the equivalent `Frac(R)`-span.

source
theorem isAlgebraic_of_isFractionRing {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [CommRing R] [CommRing S] [Field K] [CommRing L] [Algebra R S] [Algebra R K] [Algebra R L] [Algebra S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] [IsFractionRing S L] [Algebra.IsIntegral R S] :
Algebra.IsAlgebraic K L