adjoin_root_eq_top_of_isSplittingField

English

Under the isSplittingField hypothesis, the algebra generated by a root equals the top subalgebra of the ambient algebra.

Русский

При гипотезе IsSplittingField, алгебра, порождаемая корнем, равна верху подалгебры окружавшего поля.

LaTeX

$$$\\text{Algebra.adjoin } K\\{\\alpha\\} = \\top$$$

Lean4

theorem adjoin_root_eq_top_of_isSplittingField : Algebra.adjoin K { α } = ⊤ :=
  by
  apply
    Subalgebra.map_injective (B := K[n√a]) (f := (adjoinRootXPowSubCEquiv hζ H hα).symm)
      (adjoinRootXPowSubCEquiv hζ H hα).symm.injective
  rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgHom.coe_coe, adjoinRootXPowSubCEquiv_symm_eq_root, adjoinRoot_eq_top]

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