# Integral and algebraic elements of a fraction field #

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

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

coeffIntegerNormalization p gives the coefficients of the polynomial integerNormalization p

Equations
• = if hi : i p.support then else 0
Instances For
theorem IsLocalization.coeffIntegerNormalization_of_not_mem_support {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) (h : p.coeff i = 0) :
theorem IsLocalization.coeffIntegerNormalization_mem_support {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) (h : ) :
i p.support
noncomputable def IsLocalization.integerNormalization {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) :

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

Equations
• = ip.support,
Instances For
@[simp]
theorem IsLocalization.integerNormalization_coeff {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) :
.coeff i =
theorem IsLocalization.integerNormalization_spec {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) :
∃ (b : M), ∀ (i : ), () (.coeff i) = b p.coeff i
theorem IsLocalization.integerNormalization_map_to_map {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) :
∃ (b : M), = b p
theorem IsLocalization.integerNormalization_eval₂_eq_zero {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {R' : Type u_4} [CommRing R'] (g : S →+* R') (p : ) {x : R'} (hx : = 0) :
Polynomial.eval₂ (g.comp ()) x = 0
theorem IsLocalization.integerNormalization_aeval_eq_zero {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {R' : Type u_4} [CommRing R'] [Algebra R R'] [Algebra S R'] [IsScalarTower R S R'] (p : ) {x : R'} (hx : () p = 0) :
theorem IsFractionRing.integerNormalization_eq_zero_iff {A : Type u_4} {K : Type u_5} [] [] [] [Algebra A K] [] {p : } :
p = 0
theorem IsFractionRing.isAlgebraic_iff (A : Type u_4) (K : Type u_5) (C : Type u_6) [] [] [] [Algebra A K] [] [] [Algebra A C] [Algebra K C] [] {x : C} :

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

theorem IsFractionRing.comap_isAlgebraic_iff {A : Type u_4} {K : Type u_5} {C : Type u_6} [] [] [] [Algebra A K] [] [] [Algebra A C] [Algebra K C] [] :

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

theorem RingHom.isIntegralElem_localization_at_leadingCoeff {R : Type u_6} {S : Type u_7} [] [] (f : R →+* S) (x : S) (p : ) (hf : = 0) (M : ) (hM : p.leadingCoeff M) {Rₘ : Type u_8} {Sₘ : Type u_9} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [IsLocalization () Sₘ] :
().IsIntegralElem ((algebraMap S Sₘ) x)
theorem is_integral_localization_at_leadingCoeff {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [] {x : S} (p : ) (hp : () p = 0) (hM : p.leadingCoeff M) :
(IsLocalization.map 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

theorem isIntegral_localization {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [] [] :
(IsLocalization.map 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

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

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.

theorem IsIntegralClosure.isFractionRing_of_finite_extension (A : Type u_4) (K : Type u_5) [] [] (L : Type u_6) [] [] [Algebra A K] [Algebra A L] [] (C : Type u_7) [] [] [Algebra C L] [] [Algebra A C] [] [Algebra K 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.

theorem integralClosure.isFractionRing_of_algebraic {A : Type u_4} [] [] {L : Type u_6} [] [Algebra A L] [] (inj : ∀ (x : A), () x = 0x = 0) :
IsFractionRing (()) 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.

theorem integralClosure.isFractionRing_of_finite_extension {A : Type u_4} (K : Type u_5) [] [] (L : Type u_6) [] [] [Algebra A K] [] [Algebra A L] [Algebra K L] [] [] :
IsFractionRing (()) 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.

theorem IsFractionRing.isAlgebraic_iff' (R : Type u_1) [] (S : Type u_2) [] [Algebra R S] (K : Type u_5) [] [] [] [Algebra R K] [Algebra S K] [] [] [] :

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

theorem IsFractionRing.ideal_span_singleton_map_subset (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] {K : Type u_5} {L : Type u_6} [] [] [] [] [Algebra R K] [Algebra R L] [Algebra S L] [] [] [Algebra K L] [] [] {a : S} {b : Set S} [] (inj : Function.Injective ()) (h : (Ideal.span {a}) ()) :
(Ideal.span {() a}) (Submodule.span K (() '' 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.

theorem isAlgebraic_of_isLocalization {R : Type u_6} [] (M : ) (S : Type u_7) [] [] [Algebra R S] [] :
theorem isAlgebraic_of_isFractionRing {R : Type u_6} {S : Type u_7} (K : Type u_8) (L : Type u_9) [] [] [] [] [Algebra R S] [Algebra R K] [Algebra R L] [Algebra S L] [Algebra K L] [] [] [] [] :