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

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 : ℕ) :

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

source

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 : Polynomial.coeff p i = 0) :

IsLocalization.coeffIntegerNormalization M p i = 0

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 : IsLocalization.coeffIntegerNormalization M p i ≠ 0) :

i ∈ Polynomial.support p

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 = Finset.sum (Polynomial.support p) fun i => ↑(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 : ℕ) :

Polynomial.coeff (IsLocalization.integerNormalization M p) i = IsLocalization.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, ∀ (i : ℕ), ↑(algebraMap R S) (Polynomial.coeff (IsLocalization.integerNormalization M p) i) = ↑b • Polynomial.coeff p 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, Polynomial.map (algebraMap R S) (IsLocalization.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_4} [CommRing R'] (g : S →+* R') (p : Polynomial S) {x : R'} (hx : Polynomial.eval₂ g x p = 0) :

Polynomial.eval₂ (RingHom.comp g (algebraMap R S)) x (IsLocalization.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_4} [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) (IsLocalization.integerNormalization M p) = 0

source

theorem IsFractionRing.integerNormalization_eq_zero_iff {A : Type u_4} {K : Type u_5} [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_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} :

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_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] :

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_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ₘ] :

RingHom.IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(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_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) :

RingHom.IsIntegralElem (IsLocalization.map Sₘ (algebraMap R S) (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M))) (↑(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_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) :

RingHom.IsIntegral (IsLocalization.map Sₘ (algebraMap R S) (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))

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_6} {S : Type u_7} [CommRing R] [CommRing S] {f : R →+* S} (hf : RingHom.IsIntegral f) (M : Submonoid R) :

RingHom.IsIntegral (IsLocalization.map (Localization (Submonoid.map (↑f) M)) f (_ : M ≤ Submonoid.comap (↑f) (Submonoid.map (↑f) M)))

source

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 : Polynomial.leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)) :

Polynomial.scaleRoots p (↑(algebraMap R Rₘ) ↑(IsLocalization.commonDenom M (Polynomial.support p) (Polynomial.coeff p))) ∈ 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_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)

source

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 = 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_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] :

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_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 = 0 → x = 0) :

IsFractionRing { x // x ∈ 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_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] :

IsFractionRing { x // x ∈ 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_5) [Field K] [IsDomain R] [IsDomain S] [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_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.