English
A supremum (join) of a family of normal extensions is normal.
Русский
Объединение множества нормальных расширений нормально.
LaTeX
$$Normal F (⨆ i, t i : IntermediateField F K)$$
Lean4
/-- A compositum of normal extensions is normal. -/
instance normal_iSup {ι : Type*} (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] :
Normal F (⨆ i, t i : IntermediateField F K) :=
by
refine { toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }
obtain ⟨s, hx⟩ := exists_finset_of_mem_supr'' (fun i => (h i).1) x.2
let E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet K)
have hF : Normal F E :=
by
haveI : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) :=
by
refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
· exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
· exact Polynomial.splits_comp_of_splits _ (algebraMap (t i.1) K) ((h i.1).splits i.2)
apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)
have hE : E ≤ ⨆ i, t i := by
refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_
rw [adjoin_le_iff, ← image_rootSet ((h i.1).splits i.2) (t i.1).val]
exact fun _ ⟨a, _, h⟩ => h ▸ a.2
have := hF.splits ⟨x, hx⟩
rw [minpoly_eq, Subtype.coe_mk, ← minpoly_eq] at this
exact Polynomial.splits_comp_of_splits _ (inclusion hE).toRingHom this
