of_separable_splitting_field — Mathlib

English

If p is separable and E is a splitting field of p over F, then E/F is Galois.

Русский

Если p разделим и E является разложением p над F, то E/F галуа.

LaTeX

$$$p.Separable \wedge p.IsSplittingField(F,E) \Rightarrow E/F \text{ is Galois}$$$

Lean4

theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) : IsGalois F E :=
  by
  haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E p
  letI := Classical.decEq E
  let s := p.rootSet E
  have adjoin_root : IntermediateField.adjoin F s = ⊤ :=
    by
    apply IntermediateField.toSubalgebra_injective
    rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
    apply IntermediateField.algebra_adjoin_le_adjoin
  let P : IntermediateField F E → Prop := fun K => Nat.card (K →ₐ[F] E) = finrank F K
  suffices P (IntermediateField.adjoin F s) by
    rw [adjoin_root] at this
    apply of_card_aut_eq_finrank
    rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
    exact
      Nat.card_congr
        ((algEquivEquivAlgHom F E).toEquiv.trans (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))
  apply IntermediateField.induction_on_adjoin_finset _ P
  · have key :=
      IntermediateField.card_algHom_adjoin_integral F (K := E) (show IsIntegral F (0 : E) from isIntegral_zero)
    rw [IsSeparable, minpoly.zero, Polynomial.natDegree_X] at key
    specialize key Polynomial.separable_X (Polynomial.splits_X (algebraMap F E))
    rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
    refine Eq.trans ?_ key
    apply Nat.card_congr
    rw [IntermediateField.adjoin_zero]
  intro K x hx hK
  simp only [P] at *
  rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK, finrank_mul_finrank]
  symm
  refine LinearEquiv.finrank_eq ?_
  rfl

Похожие утверждения