English
If f ∈ F[X] is separable and irreducible, then for any purely inseparable extension F/E, f mapped to E remains irreducible.
Русский
Если f ∈ F[X] сепарабелен и неприводим, то отображение в E сохраняет неприводимость.
LaTeX
$$Separable(f) ∧ Irreducible(f) ⇒ Irreducible(f.map(algebraMap F E))$$
Lean4
/-- If `E / F` is a purely inseparable field extension, `f` is a separable irreducible polynomial
over `F`, then it is also irreducible over `E`. -/
theorem map_irreducible_of_isPurelyInseparable {f : F[X]} (hsep : f.Separable) (hirr : Irreducible f)
[IsPurelyInseparable F E] : Irreducible (f.map (algebraMap F E)) :=
by
let K := AlgebraicClosure E
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero K f (natDegree_pos_iff_degree_pos.1 hirr.natDegree_pos).ne'
have ha : Associated f (minpoly F x) :=
by
have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩
have ha' : Associated (f.map (algebraMap F E)) ((minpoly F x).map (algebraMap F E)) :=
ha.map (mapRingHom (algebraMap F E)).toMonoidHom
have heq := minpoly.map_eq_of_isSeparable_of_isPurelyInseparable E x (ha.separable hsep)
rw [ha'.irreducible_iff, heq]
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)
