# Documentation

Mathlib.RingTheory.Localization.Integral

# 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

Instances For
theorem IsLocalization.coeffIntegerNormalization_of_not_mem_support {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) (h : = 0) :
theorem IsLocalization.coeffIntegerNormalization_mem_support {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) (h : ) :
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

Instances For
@[simp]
theorem IsLocalization.integerNormalization_coeff {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) (i : ) :
theorem IsLocalization.integerNormalization_spec {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) :
b, ∀ (i : ), ↑() () = b
theorem IsLocalization.integerNormalization_map_to_map {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (p : ) :
b, = 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) :
= 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) :
= 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 : ) {Rₘ : Type u_8} {Sₘ : Type u_9} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [] [Algebra S Sₘ] [IsLocalization () Sₘ] :
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 : ) :

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ₘ] [] (H : ) :

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 : ) (M : ) :
theorem IsLocalization.scaleRoots_commonDenom_mem_lifts {R : Type u_1} [] (M : ) {Rₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [] (p : ) (hp : ) :
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, 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] [] (alg : ) (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] (alg : ) (inj : ∀ (x : A), ↑() x = 0x = 0) :
IsFractionRing { x // x } 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 { x // x } 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} (alg : ) (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.