English
For a suitable setup with a finite-dimensional separable extension, the sum over embeddings σ of the transformed minpolyDiv multiplied by x^r yields X^r in E[X].
Русский
В рамках конечномерного отделения, сумма по встраиваниям σ преобразованной minpolyDiv, умноженной на x^r, сводится к X^r в E[X].
LaTeX
$$$\sum_{\sigma: L \to_{{K}} E} \big( (x^r / aeval\ x\ (\operatorname{derivative}(\minpoly K x)) ) \cdot \minpolyDiv K x \big)^{\mapsto} = X^r$$
Lean4
theorem sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L]
[Algebra.IsSeparable K L] {x : L} (hxL : Algebra.adjoin K { x } = ⊤) {r : ℕ} (hr : r < finrank K L) :
∑ σ : L →ₐ[K] E, ((x ^ r / aeval x (derivative <| minpoly K x)) • minpolyDiv K x).map σ = (X ^ r : E[X]) := by
classical
rw [← sub_eq_zero]
have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
· intro σ
simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finset_sum, eval_smul, eval_map,
eval₂_minpolyDiv_self, this.eq_iff, smul_eq_mul, mul_ite, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, ite_true,
eval_X_pow]
rw [sub_eq_zero, div_mul_cancel₀]
rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]
exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
· refine (Polynomial.natDegree_sub_le _ _).trans_lt (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
· simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, Function.comp_apply, Finset.mem_univ,
forall_true_left, Finset.fold_max_lt, AlgHom.card]
refine ⟨finrank_pos, ?_⟩
intro σ
exact
((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le (minpoly.natDegree_le _))
· rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
