English
The intersection of a family of normal extensions is normal.
Русский
Пересечение семейства нормальных расширений нормально.
LaTeX
$$Normal F (⨅ i, t i : IntermediateField F K)$$
Lean4
/-- An intersection of normal extensions is normal. -/
@[stacks 09HP]
instance normal_iInf {ι : Type*} [hι : Nonempty ι] (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] :
Normal F (⨅ i, t i : IntermediateField F K) :=
by
refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }
· let f := inclusion (iInf_le t hι.some)
exact Algebra.IsAlgebraic.of_injective f f.injective
· have hx : ∀ i, Splits (algebraMap F (t i)) (minpoly F x) :=
by
intro i
rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
exact (h i).splits' (inclusion (iInf_le t i) x)
simp only [splits_iff_mem (splits_of_isScalarTower K (hx hι.some))] at hx ⊢
rintro y hy - ⟨-, ⟨i, rfl⟩, rfl⟩
exact hx i y hy
