English
The splitting field of a polynomial over a field F is a normal extension of F.
Русский
Разложимое поле многочлена над полем F является нормальным расширением F.
LaTeX
$$Normal F p.SplittingField$$
Lean4
@[stacks 09HU "Normal part"]
theorem of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : Normal F E :=
by
rcases eq_or_ne p 0 with (rfl | hp)
· have := hFEp.adjoin_rootSet
rw [rootSet_zero, Algebra.adjoin_empty] at this
exact Normal.of_algEquiv (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))
refine normal_iff.mpr fun x ↦ ?_
haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
have hx := IsIntegral.of_finite F x
let L := (p * minpoly F x).SplittingField
have hL := splits_of_splits_mul' _ ?_ (SplittingField.splits (p * minpoly F x))
· let j : E →ₐ[F] L := IsSplittingField.lift E p hL.1
refine ⟨hx, splits_of_comp _ (j : E →+* L) (j.comp_algebraMap ▸ hL.2) fun a ha ↦ ?_⟩
rw [j.comp_algebraMap] at ha
letI : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra
let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
· change a ∈ j.range
rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
· rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]; exact hL.1
· rw [Polynomial.map_ne_zero_iff (algebraMap F L).injective, mul_ne_zero_iff]
exact ⟨hp, minpoly.ne_zero hx⟩
