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
  • One or more equations did not get rendered due to their size.
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_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 : Polynomial.leadingCoeff p 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ₘ] :
      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 : Polynomial.leadingCoeff p M) :

      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ₘ] (H : Algebra.IsIntegral R S) :

      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 : RingHom.IsIntegral f) (M : Submonoid 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, 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] (alg : 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] (alg : 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.

      theorem integralClosure.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] [IsFractionRing A K] [Algebra A 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 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} (alg : 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.