English
The Steinitz theorem states that an algebraic extension E/F has a primitive element if and only if there are only finitely many intermediate fields between E and F.
Русский
Теорема Стейнистца утверждает, что алгебраическое расширение E/F имеет примитивный элемент тогда и только тогда, когда существует конечное число промежуточных полей между E и F.
LaTeX
$$$(\text{Algebra.IsAlgebraic } F E) \wedge (\exists \alpha, F\langle \alpha\rangle = \top) \iff Finite(\text{IntermediateField } F E)$$$
Lean4
theorem finite_intermediateField_of_exists_primitive_element [Algebra.IsAlgebraic F E] (h : ∃ α : E, F⟮α⟯ = ⊤) :
Finite (IntermediateField F E) :=
by
haveI := FiniteDimensional.of_exists_primitive_element F E h
obtain ⟨α, hprim⟩ := h
let f : F[X] := minpoly F α
let G :=
{ g : E[X] // g.Monic ∧ g ∣ f.map (algebraMap F E) }
-- Then `f` has only finitely many monic factors
have hfin : Finite G :=
@Finite.of_fintype _ <|
fintypeSubtypeMonicDvd (f.map (algebraMap F E)) <|
map_ne_zero
(minpoly.ne_zero_of_finite F α)
-- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α` over `K`
-- which is a monic factor of `f`
let g : IntermediateField F E → G := fun K ↦
⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| .of_finite K α).map _,
by
convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
rw [Polynomial.map_map]; rfl⟩
-- The map `K ↦ g` is injective
have hinj : Function.Injective g := fun K K' heq ↦
by
rw [Subtype.mk.injEq] at heq
apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq
exact Finite.of_injective g hinj
