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} [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
Instances For
    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) :

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

    Equations
    Instances For
      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) ((IsLocalization.integerNormalization M p).coeff i) = b p.coeff i
      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_4} [CommRing R'] (g : S →+* R') (p : Polynomial S) {x : R'} (hx : Polynomial.eval₂ g x p = 0) :
      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_4} [CommRing R'] [Algebra R R'] [Algebra S R'] [IsScalarTower R S R'] (p : Polynomial S) {x : R'} (hx : (Polynomial.aeval x) p = 0) :
      theorem IsFractionRing.isAlgebraic_iff (A : Type u_4) (K : Type u_5) (C : Type u_6) [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} :

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

      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} [CommRing R] [CommRing 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_8} {Sₘ : Type u_9} [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)
      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_4} {Sₘ : Type u_5} [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

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

      theorem isIntegral_localization' {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsIntegral) (M : Submonoid R) :
      (IsLocalization.map (Localization (Submonoid.map (↑f) M)) f ).IsIntegral
      theorem IsLocalization.scaleRoots_commonDenom_mem_lifts {R : Type u_1} [CommRing R] (M : Submonoid R) {Rₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] (p : Polynomial Rₘ) (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} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_4} [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)
      theorem IsIntegralClosure.isFractionRing_of_algebraic (A : Type u_4) [CommRing A] [IsDomain A] {L : Type u_6} [Field L] [Algebra A L] (C : Type u_7) [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 = 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) [CommRing A] [IsDomain A] (L : Type u_6) [Field K] [Field L] [Algebra A K] [Algebra A L] [IsFractionRing A K] (C : Type u_7) [CommRing C] [IsDomain C] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional 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} [CommRing A] [IsDomain A] {L : Type u_6} [Field L] [Algebra A L] [Algebra.IsAlgebraic A L] (inj : ∀ (x : A), (algebraMap A L) x = 0x = 0) :

      If the field L is an algebraic extension of the integral domain A, the integral closure of A in L has fraction field 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.

      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) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {K : Type u_5} {L : Type u_6} [IsDomain R] [IsDomain S] [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra S L] [IsIntegralClosure S R L] [IsFractionRing S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] {a : S} {b : Set S} [Algebra.IsAlgebraic R L] (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.

      theorem isAlgebraic_of_isFractionRing {R : Type u_6} {S : Type u_7} (K : Type u_8) (L : Type u_9) [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] :