English
Let R be integrally closed, and B a power basis with B.gen integral over R. Then if z is integral over R and p divides certain coefficients, z lies in the adjoin of R with the generator B.gen.
Русский
Пусть R интеграло замкнуто и B генератор степени, тогда если z интеграл над R и коэффициенты удовлетворяют условиям, то z принадлежит адуйну R с B.gen.
LaTeX
$$$\\text{mem\_adjoin\_of\_smul\_prime\_pow\_smul\_of\_minpoly\_isEisensteinAt}$$$
Lean4
/-- Let `K` be the field of fraction of an integrally closed domain `R` and let `L` be an extension
of `K`, generated by an integral power basis `B` such that the minimal polynomial of `B.gen` is
Eisenstein at `p`. Given `z : L` integral over `R`, if `Q : R[X]` is such that
`aeval B.gen Q = p • z`, then `p ∣ Q.coeff 0`. -/
theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis K L} (hp : Prime p)
(hBint : IsIntegral R B.gen) {z : L} {Q : R[X]} (hQ : aeval B.gen Q = p • z) (hzint : IsIntegral R z)
(hei : (minpoly R B.gen).IsEisensteinAt 𝓟) : p ∣ Q.coeff 0 := by
-- First define some abbreviations.
letI := B.finite
let P := minpoly R B.gen
obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'
have finrank_K_L : Module.finrank K L = B.dim := B.finrank
have deg_K_P : (minpoly K B.gen).natDegree = B.dim := B.natDegree_minpoly
have deg_R_P : P.natDegree = B.dim := by
rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
(minpoly.monic hBint).natDegree_map (algebraMap R K)]
choose! f hf using
hei.isWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le (minpoly.aeval R B.gen) (minpoly.monic hBint)
simp only [P, (minpoly.monic hBint).natDegree_map, deg_R_P] at hf
suffices p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
by
have hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0 := fun h =>
hei.notMem ((span_singleton_pow p 2).symm ▸ Ideal.mem_span_singleton.2 h)
refine @Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd R _ _ _ _ n hp (?_ : _ ∣ _) hndiv
convert (IsUnit.dvd_mul_right ⟨(-1) ^ (n.succ * n), rfl⟩).mpr this using 1
push_cast
ring_nf
rw [mul_comm _ 2, pow_mul, neg_one_sq, one_pow, mul_one]
-- We claim the quotient of `Q^n * _` by `p^n` is the following `r`:
have aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n := by grind
have hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) :=
by
refine (hzint.mul (hBint.pow _)).sub (.sum _ fun i hi => .smul _ ?_)
exact adjoin_le_integralClosure hBint (hf _ (aux i hi)).1
obtain ⟨r, hr⟩ := isIntegral_iff.1 (isIntegral_norm K hintsum)
use r
apply IsFractionRing.injective R K
simp only [map_mul, map_pow, map_neg, map_one]
-- Both sides are actually norms:
calc
_ = norm K (Q.coeff 0 • B.gen ^ n) := ?_
_ = norm K (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) :=
(congr_arg (norm K) (eq_sub_of_add_eq ?_))
_ = _ := ?_
· simp only [Algebra.smul_def, algebraMap_apply R K L, Algebra.norm_algebraMap, map_mul, map_pow, finrank_K_L,
PowerBasis.norm_gen_eq_coeff_zero_minpoly, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, coeff_map,
← hn]
ring
swap
·
simp_rw [← smul_sum, ← smul_sub, Algebra.smul_def p, algebraMap_apply R K L, map_mul, Algebra.norm_algebraMap,
finrank_K_L, hr, ← hn]
calc
_ = (Q.coeff 0 • ↑1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n := ?_
_ = (Q.coeff 0 • B.gen ^ 0 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n := by
rw [pow_zero]
_ = aeval B.gen Q * B.gen ^ n := ?_
_ = _ := by rw [hQ, Algebra.smul_mul_assoc]
· have : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n) :=
by
intro i hi
rw [← pow_add, ← (hf _ (aux i hi)).2, ← Algebra.smul_def, smul_smul, mul_comm _ p, smul_smul]
simp only [add_mul, smul_mul_assoc, one_mul, sum_mul, sum_congr rfl this]
· rw [aeval_eq_sum_range, Finset.add_sum_erase (range (Q.natDegree + 1)) fun i => Q.coeff i • B.gen ^ i]
simp
