English
Given an irreducible X^n − C a, the splitting field of this polynomial is generated by adjoining n-th root of a and its conjugates.
Русский
При ирредуцируемости X^n − C a, разложение поля образуется за счёт присоединения n-й корня a и его сопряжённых.
LaTeX
$$$\\text{splitting field generation}$ via $K[n\\sqrt[n]{a}]$$$
Lean4
/-- Suppose `L/K` is the splitting field of `Xⁿ - a`, then a choice of `ⁿ√a` gives an equivalence of
`L` with `K[n√a]`. -/
noncomputable def adjoinRootXPowSubCEquiv (hζ : (primitiveRoots n K).Nonempty) (H : Irreducible (X ^ n - C a))
(hα : α ^ n = algebraMap K L a) : K[n√a] ≃ₐ[K] L :=
AlgEquiv.ofBijective (AdjoinRoot.liftHom (X ^ n - C a) α (by simp [hα])) <|
by
haveI := Fact.mk H
letI := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
refine ⟨(liftHom (X ^ n - C a) α _).injective, ?_⟩
rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a), eq_comm, adjoin_rootSet_eq_range,
IsSplittingField.adjoin_rootSet]
exact IsSplittingField.splits _ _
