English
If E/F is purely inseparable, and a ∈ K is separable over F, then the minimal polynomial of a maps to the minimal polynomial over E via the algebra map, i.e., minpoly_E(a) = (minpoly_F(a))^map(algebraMap F E).
Русский
Если E/F чисто инsep, и a ∈ K сепарабельен над F, тогда минимальный полином a над E равен образу минполинома над F через алгебраическое отображение.
LaTeX
$$minpoly_E(a) = (minpoly_F(a)).map( algebraMap F E )$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any subset `S` of `K` such that `F(S) / F` is algebraic, the `E(S) / E` and `F(S) / F` have
the same separable degree. -/
theorem sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (S : Set K) [Algebra.IsAlgebraic F (adjoin F S)]
[IsPurelyInseparable F E] : sepDegree E (adjoin E S) = sepDegree F (adjoin F S) :=
by
set M := adjoin F S
set L := adjoin E S
let E' := (IsScalarTower.toAlgHom F E K).fieldRange
let j : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
have hi : M ≤ L.restrictScalars F :=
by
rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]
exact adjoin.mono _ _ _ Set.subset_union_right
let i : M →+* L := Subsemiring.inclusion hi
letI : Algebra M L := i.toAlgebra
letI : SMul M L := Algebra.toSMul
haveI : IsScalarTower F M L := IsScalarTower.of_algebraMap_eq (congrFun rfl)
haveI : IsPurelyInseparable M L := by
change IsPurelyInseparable M (extendScalars hi)
obtain ⟨q, _⟩ := ExpChar.exists F
have : extendScalars hi = adjoin M (E' : Set K) :=
restrictScalars_injective F <| by
conv_lhs =>
rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv (E := K) j rfl, ← adjoin_self F E',
adjoin_adjoin_comm]
rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q]
rintro x ⟨y, hy⟩
obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
refine ⟨n, algebraMap F M z, ?_⟩
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L
rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h
rw [Cardinal.lift_injective h, ← sepDegree_mul_sepDegree_of_isAlgebraic F M L,
IsPurelyInseparable.sepDegree_eq_one M L, mul_one]
