Integral and algebraic elements of a fraction field #
Implementation notes #
See Mathlib/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
theorem
IsLocalization.coeffIntegerNormalization_of_coeff_zero
{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 : p.coeff i = 0)
:
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 : coeffIntegerNormalization M p i ≠ 0)
:
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
@[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 : ℕ)
:
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) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
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 : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
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_3}
[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_3}
[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.integerNormalization_eq_zero_iff
{A : Type u_3}
{K : Type u_4}
[CommRing A]
[IsDomain A]
[Field K]
[Algebra A K]
[IsFractionRing A K]
{p : Polynomial K}
:
theorem
IsFractionRing.isAlgebraic_iff
(A : Type u_3)
(K : Type u_4)
(C : Type u_5)
[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.
theorem
IsFractionRing.comap_isAlgebraic_iff
{A : Type u_3}
{K : Type u_4}
{C : Type u_5}
[CommRing A]
[IsDomain A]
[Field K]
[Algebra A K]
[IsFractionRing A K]
[CommRing C]
[Algebra A C]
[Algebra K C]
[IsScalarTower A 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_5}
{S : Type u_6}
[CommSemiring R]
[CommSemiring 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_7}
{Sₘ : Type u_8}
[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_3}
{Sₘ : Type u_4}
[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_3}
{Sₘ : Type u_4}
[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_5}
{S : Type u_6}
[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_3}
[CommRing Rₘ]
[Algebra R Rₘ]
[IsLocalization M Rₘ]
(p : Polynomial Rₘ)
(hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range)
:
p.scaleRoots ((algebraMap R Rₘ) ↑(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_3}
[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
IsLocalization.exists_isIntegral_smul_of_isIntegral_map
{R : Type u_5}
{S : Type u_6}
{Sₘ : Type u_7}
[CommRing R]
[CommRing S]
[CommRing Sₘ]
[Algebra R S]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
(M : Submonoid R)
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
{x : S}
(hx : IsIntegral R ((algebraMap S Sₘ) x))
:
∃ m ∈ M, IsIntegral R (m • x)
If t is R-integral in S[M⁻¹] where M is a submonoid of R,
then m • t is integral in S for some m ∈ M.
theorem
IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap
{R : Type u_5}
{S : Type u_6}
{Sₘ : Type u_7}
[CommRing R]
[CommRing S]
[CommRing Sₘ]
[Algebra R S]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
{r : S}
(hr : IsIntegral R r)
[Away r Sₘ]
{x : S}
(hx : IsIntegral R ((algebraMap S Sₘ) x))
:
∃ (n : ℕ), IsIntegral R (r ^ n * x)
If t is R-integral in S[1/r] where r : S is integral over R,
then r ^ n • t is integral in S for some n.
theorem
IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_mk'
{R : Type u_5}
{S : Type u_6}
{Sₘ : Type u_7}
[CommRing R]
[CommRing S]
[CommRing Sₘ]
[Algebra R S]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
{r : S}
(hr : IsIntegral R r)
[Away r Sₘ]
{x : S}
{a : ↥(Submonoid.powers r)}
(hx : IsIntegral R (mk' Sₘ x a))
:
∃ (n : ℕ), IsIntegral R (r ^ n * x)
theorem
isIntegral_of_isIntegral_adjoin_of_mul_eq_one
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(t s : S)
(hst : s * t = 1)
(ht : IsIntegral (↥(Algebra.adjoin R {s})) t)
:
IsIntegral R t
If t is integral over R[1/t], then it is integral over R.
theorem
IsLocalization.Away.isIntegral_of_isIntegral_map
{R : Type u_5}
{S : Type u_6}
{Sₘ : Type u_7}
[CommRing R]
[CommRing S]
[CommRing Sₘ]
[Algebra R S]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
(x : S)
[Away x Sₘ]
(hx : IsIntegral R ((algebraMap S Sₘ) x))
:
IsIntegral R x
If t is integral in S[1/t], then it is integral in S.
theorem
IsIntegralClosure.isFractionRing_of_algebraic
(A : Type u_3)
[CommRing A]
{L : Type u_5}
[Field L]
[Algebra A L]
(C : Type u_6)
[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 = 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.
theorem
IsIntegralClosure.isFractionRing_of_finite_extension
(A : Type u_3)
(K : Type u_4)
[CommRing A]
(L : Type u_5)
[Field K]
[Field L]
[Algebra A K]
[Algebra A L]
[IsFractionRing A K]
(C : Type u_6)
[CommRing C]
[IsDomain C]
[Algebra C L]
[IsIntegralClosure C A L]
[Algebra A C]
[IsScalarTower A C L]
[IsDomain A]
[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.
theorem
integralClosure.isFractionRing_of_algebraic
{A : Type u_3}
[CommRing A]
{L : Type u_5}
[Field L]
[Algebra A L]
[Algebra.IsAlgebraic A L]
(inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0)
:
IsFractionRing (↥(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.
theorem
integralClosure.isFractionRing_of_finite_extension
{A : Type u_3}
(K : Type u_4)
[CommRing A]
(L : Type u_5)
[Field K]
[Field L]
[Algebra A K]
[IsFractionRing A K]
[IsDomain A]
[Algebra A L]
[Algebra K L]
[IsScalarTower A K L]
[FiniteDimensional K L]
:
IsFractionRing (↥(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.
theorem
IsLocalization.integralClosure
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
{Rf : Type u_5}
{Sf : Type u_6}
[CommRing Rf]
[CommRing Sf]
[Algebra R Rf]
[Algebra S Sf]
[Algebra Rf Sf]
[Algebra R Sf]
[IsScalarTower R S Sf]
[IsScalarTower R Rf Sf]
(M : Submonoid R)
[IsLocalization M Rf]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sf]
[Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
[IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf]
[IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
:
IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) ↥(integralClosure Rf Sf)
Taking integral closure commutes with localizations.
theorem
IsLocalization.Away.integralClosure
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
{Rf : Type u_5}
{Sf : Type u_6}
[CommRing Rf]
[CommRing Sf]
[Algebra R Rf]
[Algebra S Sf]
[Algebra Rf Sf]
[Algebra R Sf]
[IsScalarTower R S Sf]
[IsScalarTower R Rf Sf]
(f : R)
[Away f Rf]
[Away ((algebraMap R S) f) Sf]
[Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
[IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf]
[IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
:
Away ((algebraMap R ↥(integralClosure R S)) f) ↥(integralClosure Rf Sf)
theorem
IsFractionRing.isAlgebraic_iff'
(R : Type u_1)
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
(K : Type u_4)
[Field K]
[IsDomain R]
[Algebra R K]
[Algebra S K]
[Module.IsTorsionFree R K]
[IsFractionRing S K]
[IsScalarTower R 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)
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
{K : Type u_4}
{L : Type u_5}
[IsDomain R]
[IsDomain S]
[Field K]
[Field L]
[Algebra R K]
[Algebra R L]
[Algebra S L]
[Algebra.IsAlgebraic R S]
[IsFractionRing S L]
[Algebra K L]
[IsScalarTower R S L]
[IsScalarTower R K L]
{a : S}
{b : Set S}
(inj : Function.Injective ⇑(algebraMap R L))
(h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R 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_5}
{S : Type u_6}
(K : Type u_7)
(L : Type u_8)
[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]
: