English
For f ∈ K[X], SplittingFieldAux f.natDegree f is a splitting field of f over K.
Русский
Для f ∈ K[X], SplittingFieldAux f.natDegree f является разворачивающим полем f над K.
LaTeX
$$$\\text{IsSplittingField }K\\; (\\text{SplittingFieldAux } f\\,\\text{natDegree } f)\\; f$$$
Lean4
theorem adjoin_rootSet (n : ℕ) :
∀ {K : Type u} [Field K],
∀ (f : K[X]) (_hfn : f.natDegree = n), Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤ :=
Nat.recOn (motive := fun n =>
∀ {K : Type u} [Field K],
∀ (f : K[X]) (_hfn : f.natDegree = n), Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
n (fun {_} _ _ _hf => Algebra.eq_top_iff.2 fun x => Subalgebra.range_le _ ⟨x, rfl⟩) fun n ih {K} _ f hfn =>
by
have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn; cases hfn
have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf; exact hndf rfl
have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0
classical
rw [rootSet_def, aroots_def]
rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add, Finset.coe_union,
Multiset.toFinset_singleton, Finset.coe_singleton, Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [Algebra.adjoin_algebraMap K (SplittingFieldAux n f.removeFactor)]
rw [AdjoinRoot.adjoinRoot_eq_top, Algebra.map_top]
-- Porting note: was `rw`
erw [IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)
(f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))]
rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]
