English
Under ha and hα, the polynomial X^{finrank(K,L)} − C a is a splitting field over K for L.
Русский
При ha и hα полином X^{finrank(K,L)} − C a является разворачивающим полем над K для L.
LaTeX
$$$\text{IsSplittingField}(K,L,X^{\mathrm{finrank}(K,L)} - C a).$$$
Lean4
theorem isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a)
(hα : K⟮α⟯ = ⊤) : IsSplittingField K L (X ^ (finrank K L) - C a) :=
by
constructor
· rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C, Polynomial.map_X]
have ⟨_, hζ⟩ := hK
rw [mem_primitiveRoots finrank_pos] at hζ
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha
· rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite K α)]
apply Algebra.adjoin_mono
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a), aeval_def, eval₂_sub,
eval₂_X_pow, eval₂_C, ha, sub_self]
