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
- IsLocalization.coeffIntegerNormalization M p i = if hi : i ∈ p.support then Classical.choose ⋯ else 0
Instances For
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 : 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 : IsLocalization.coeffIntegerNormalization M p i ≠ 0)
:
i ∈ p.support
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
- IsLocalization.integerNormalization M p = ∑ i ∈ p.support, (Polynomial.monomial i) (IsLocalization.coeffIntegerNormalization M p i)
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 : ℕ)
:
(IsLocalization.integerNormalization M p).coeff i = IsLocalization.coeffIntegerNormalization M p 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) ((IsLocalization.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) (IsLocalization.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_4}
[CommRing R']
(g : S →+* R')
(p : Polynomial S)
{x : R'}
(hx : Polynomial.eval₂ g x p = 0)
:
Polynomial.eval₂ (g.comp (algebraMap R S)) x (IsLocalization.integerNormalization M 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)
:
(Polynomial.aeval x) (IsLocalization.integerNormalization M p) = 0
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
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.
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.
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 = 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_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.
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 = 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_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 (↥(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
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
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_isLocalization
{R : Type u_6}
[CommRing R]
(M : Submonoid R)
(S : Type u_7)
[CommRing S]
[Nontrivial R]
[Algebra R S]
[IsLocalization M S]
:
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]
: