normalClosure_eq_iSup_adjoin' — Mathlib

English

If there exists a nonempty algebra homomorphism from K to L, then the normal closure equals the iSup over x in K of adjoin F rootSet of minpoly F x in L.

Русский

При наличии непустого алгебраического гомоморфизма из K в L нормальное замыкание равно iSup по x∈K от adjoin F корневого множества minpoly F x в L.

LaTeX

$$$\text{normalClosure}(F,K,L)=\big\langle x:K, adjoin F ((\minpoly F x).rootSet L)\big\rangle$$$

Lean4

theorem normalClosure_eq_iSup_adjoin' [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) :=
  by
  have ⟨φ⟩ := ne
  refine h.toIsAlgebraic.of_injective φ φ.injective |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_
  rw [← minpoly.algHom_eq _ φ.injective]
  apply h.splits

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