English
If E/F is purely inseparable and x ∈ K is separable over F, then (minpoly F x).map(algebraMap F E) = minpoly E x.
Русский
Если E/F чисто инсе, и x ∈ K сепарабель над F, то (minpoly_F x).map(algebraMap F E) = minpoly_E x.
LaTeX
$$(minpoly_F x).map(algebraMap F E) = minpoly_E x$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any element `x` of `K` separable over `F`, it has the same minimal polynomials over `F` and
over `E`. -/
theorem map_eq_of_isSeparable_of_isPurelyInseparable (x : K) (hsep : IsSeparable F x) [IsPurelyInseparable F E] :
(minpoly F x).map (algebraMap F E) = minpoly E x :=
by
have hi := IsSeparable.isIntegral hsep
have hi' : IsIntegral E x := IsIntegral.tower_top hi
refine
eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E)) (dvd_map_of_isScalarTower F E x)
(le_of_eq ?_)
have hsep' := IsSeparable.tower_top E hsep
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep'
have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯
rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi', ← finSepDegree_eq_finrank_of_isSeparable F _,
← finSepDegree_eq_finrank_of_isSeparable E _, finSepDegree_eq, finSepDegree_eq,
sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
