feat(FieldTheory/Normal): Intersection of normal extensions is normal (#15290)

This PR proves that an intersection of normal extensions is normal (we already have that a compositum of normal extensions is normal).

Author: tb65536

Mathlib/FieldTheory/Normal.lean

@@ -174,6 +174,26 @@ instance normal_sup
     Normal F (E ⊔ E' : IntermediateField F K) :=
   iSup_bool_eq (f := Bool.rec E' E) ▸ normal_iSup (h := by rintro (_|_) <;> infer_instance)
 
+/-- An intersection of normal extensions is normal -/
+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
+
+instance normal_inf
+    (E E' : IntermediateField F K) [Normal F E] [Normal F E'] :
+    Normal F (E ⊓ E' : IntermediateField F K) :=
+  iInf_bool_eq (f := Bool.rec E' E) ▸ normal_iInf (h := by rintro (_|_) <;> infer_instance)
+
 variable {F K}
 variable {L : Type*} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L]
 

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

@@ -150,6 +150,13 @@ theorem IntermediateField.splits_of_splits (h : p.Splits (algebraMap K L))
   simp_rw [← F.fieldRange_val, rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF
   exact splits_of_comp _ F.val.toRingHom h hF
 
+theorem IntermediateField.splits_iff_mem (h : p.Splits (algebraMap K L)) :
+    p.Splits (algebraMap K F) ↔ ∀ x ∈ p.rootSet L, x ∈ F := by
+  refine ⟨?_, IntermediateField.splits_of_splits h⟩
+  intro hF
+  rw [← Polynomial.image_rootSet hF F.val, Set.forall_mem_image]
+  exact fun x _ ↦ x.2
+
 theorem IsIntegral.mem_intermediateField_of_minpoly_splits {x : L} (int : IsIntegral K x)
     {F : IntermediateField K L} (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F := by
   rw [← F.fieldRange_val]; exact int.mem_range_algebraMap_of_minpoly_splits h