Embeddings of a simple field and roots of the minimal polynomial

An embedding of the simple field F⟮α⟯ into an extension K is determined by the image of its generator, which can be any root in K of minpoly F α. Mathlib's IntermediateField.algHomAdjoinIntegralEquiv expresses this using the root multiset. This file gives the corresponding equivalence for Polynomial.rootSet, the carrier used by polynomial Galois actions.

Main definitions

• TauCeti.rootSetEquivAlgHomAdjoin: the equivalence between roots of minpoly F α in K and F-embeddings F⟮α⟯ → K.

noncomputable def TauCeti.rootSetEquivAlgHomAdjoin (F : Type u_1) (K : Type u_2) [Field F] [Field K] {E : Type u_3} [Field E] [Algebra F E] [Algebra F K] (α : E) (hα : IsIntegral F α) : ↑((minpoly F α).rootSet K) ≃ (↥F⟮α⟯ →ₐ[F] K)

The roots in K of the minimal polynomial of an integral element α correspond to the F-embeddings of the simple field F⟮α⟯ into K.

Equations

• TauCeti.rootSetEquivAlgHomAdjoin F K α hα = ((Equiv.refl K).subtypeEquiv ⋯).trans (IntermediateField.algHomAdjoinIntegralEquiv F hα).symm

@[simp]

theorem TauCeti.rootSetEquivAlgHomAdjoin_apply_gen (F : Type u_1) (K : Type u_2) [Field F] [Field K] {E : Type u_3} [Field E] [Algebra F E] [Algebra F K] (α : E) (hα : IsIntegral F α) (y : ↑((minpoly F α).rootSet K)) : ((rootSetEquivAlgHomAdjoin F K α hα) y) (IntermediateField.AdjoinSimple.gen F α) = ↑y

Under rootSetEquivAlgHomAdjoin, the embedding corresponding to a root y sends the adjoined generator to y.

@[simp]

theorem TauCeti.rootSetEquivAlgHomAdjoin_symm_apply (F : Type u_1) (K : Type u_2) [Field F] [Field K] {E : Type u_3} [Field E] [Algebra F E] [Algebra F K] (α : E) (hα : IsIntegral F α) (φ : ↥F⟮α⟯ →ₐ[F] K) : ↑((rootSetEquivAlgHomAdjoin F K α hα).symm φ) = φ (IntermediateField.AdjoinSimple.gen F α)

The inverse equivalence assigns to an embedding the image of the adjoined generator.