English
Given a primitive root, irreducible X^n − C a implies the same separability after map to a suitable extension.
Русский
Дано примитивный корень, ирредуцируемость X^n − C a сохраняет разделяемость после отображения в подходящее расширение.
LaTeX
$$$(X^n - C a).Separable$$$
Lean4
/-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
`η ↦ (ⁿ√a ↦ η • ⁿ√a)`. Also see `autAdjoinRootXPowSubC` for the `AlgEquiv` version. -/
noncomputable def autAdjoinRootXPowSubCHom : rootsOfUnity n K →* (K[n√a] →ₐ[K] K[n√a])
where
toFun := fun η ↦
liftHom (X ^ n - C a) (((η : Kˣ) : K) • (root _) : K[n√a]) <|
by
have := (mem_rootsOfUnity' _ _).mp η.prop
rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow, AdjoinRoot.algebraMap_eq,
← map_pow, this, map_one, one_mul, sub_self]
map_one' := algHom_ext <| by simp
map_mul' := fun ε η ↦ algHom_ext <| by simp [mul_smul, smul_comm ((ε : Kˣ) : K)]
