mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt :
∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [inst_6 : IsScalarTower R K L]
[inst_7 : IsSeparable K L] [inst_8 : IsDomain R] [inst_9 : IsFractionRing R K] [inst_10 : IsIntegrallyClosed R]
{B : PowerBasis K L},
Prime p →
IsIntegral R B.gen →
∀ {z : L},
IsIntegral R z →
p • z ∈ Algebra.adjoin R {B.gen} →
(minpoly R B.gen).IsEisensteinAt (Submodule.span R {p}) → z ∈ Algebra.adjoin R {B.gen}
This theorem states that given an integrally closed domain `R` with its field of fractions `K`, and a separable extension `L` of `K` generated by an integral power basis `B` whose generator's minimal polynomial is Eisenstein at a prime element `p`. If a specific element `z` from `L` is integral over `R` and the product of `p` and `z` lies in the subalgebra generated by the generator of `B` over `R`, then `z` itself also lies in this subalgebra.
More concisely: Given an integrally closed domain `R`, its field of fractions `K`, a separable extension `L` generated by an integral power basis `B` with Eisenstein minimal polynomials, if an element `z` in `L` is integral over `R` and `pz` lies in the `R`-subalgebra generated by `B`, then `z` is in this `R`-subalgebra.
|
mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt
theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt :
∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [inst_6 : IsScalarTower R K L]
[inst_7 : IsSeparable K L] [inst_8 : IsDomain R] [inst_9 : IsFractionRing R K] [inst_10 : IsIntegrallyClosed R]
{B : PowerBasis K L},
Prime p →
IsIntegral R B.gen →
∀ {n : ℕ} {z : L},
IsIntegral R z →
p ^ n • z ∈ Algebra.adjoin R {B.gen} →
(minpoly R B.gen).IsEisensteinAt (Submodule.span R {p}) → z ∈ Algebra.adjoin R {B.gen}
This theorem states that given an integrally closed domain `R`, its field of fractions `K`, a separable extension `L` of `K`, an integral power basis `B` of `L` over `K` whose generator's minimal polynomial is Eisenstein at a prime element `p` of `R`, and an element `z` of `L` which is integral over `R`, if `p` raised to some power `n` and multiplied by `z` is in the subalgebra generated by the generator of `B`, then `z` is also in this subalgebra. This theorem, together with `Algebra.discr_mul_isIntegral_mem_adjoin`, can often be used to compute the ring of integers of `L`.
More concisely: If `R` is an integrally closed domain, `L` is a separable extension of `R`'s field of fractions `K`, `B` is a power basis of `L` over `K` with Eisenstein minimal polynomial at prime `p` of `R`, and `z` is integral over `R`, then `p^n * z` in the subalgebra generated by `B`'s generator implies `z` is in this subalgebra.
|
dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt
theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt :
∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [inst_6 : IsScalarTower R K L]
[inst_7 : IsSeparable K L] [inst_8 : IsDomain R] [inst_9 : IsFractionRing R K] [inst_10 : IsIntegrallyClosed R]
{B : PowerBasis K L},
Prime p →
IsIntegral R B.gen →
∀ {z : L} {Q : Polynomial R},
(Polynomial.aeval B.gen) Q = p • z →
IsIntegral R z → (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p}) → p ∣ Q.coeff 0
This theorem states that for a given field of fraction `K` of an integrally closed domain `R` and a separable extension `L` of `K` generated by an integral power basis `B`, where the minimal polynomial of `B.gen` is Eisenstein at `p`. If there exists an element `z` in `L` that is integral over `R` and a polynomial `Q` in `R[X]` such that the evaluation of `Q` at `B.gen` equals `p` times `z`, then `p` is a divisor of the zeroth coefficient of `Q`. This holds true if `z` is integral over `R` and the minimal polynomial of `B.gen` is Eisenstein over the submodule spanned by `p` in `R`.
More concisely: If `z` is an integral element of a separable extension `L` of an integrally closed domain `R`, generated by an integral power basis `B` with Eisenstein minimal polynomial, such that `p` is the evaluation of some polynomial `Q` at `B.gen` with integral `z`, then the zeroth coefficient of `Q` is divisible by `p`.
|