normalClosure_eq_iSup_adjoin_of_splits

English

If K/F is algebraic, IsNormalClosure F K L is equivalent to saying that every minpoly F x splits in L together with normalClosure F K L = ⊤.

Русский

Если K/F алгебраическое, IsNormalClosure F K L эквивалентно тому, что каждый minpoly F x распадается в L и normalClosure F K L = ⊤.

LaTeX

$$$IsNormalClosure F K L \iff \Big( \forall x:K,\minpoly F x \text{ splits in }L\Big) \land normalClosure F K L = \top$$$

Lean4

theorem normalClosure_eq_iSup_adjoin_of_splits :
    normalClosure F K L = ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L) :=
  normalClosure_le_iSup_adjoin.antisymm <|
    iSup_le fun x ↦
      IntermediateField.adjoin_le_iff.mpr fun _ hy ↦
        let ⟨φ, hφ⟩ :=
          IntermediateField.exists_algHom_of_splits_of_aeval (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, splits x⟩)
            (mem_rootSet.mp hy).2
        le_iSup AlgHom.fieldRange φ ⟨x, hφ⟩

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