Embeddings of a simple field indexed by root-stabilizer cosets

Let x lie in a normal extension of F, and put N for the normal closure of F⟮x⟯ in that extension. The F-embeddings of F⟮x⟯ into N are determined by the image of the generator, which is a root of minpoly F x. By orbit-stabilizer, they are therefore indexed by the cosets G / H of a root stabilizer H, either in G = Gal(N/F) or in the polynomial Galois group of minpoly F x. These identifications respect the Galois action by postcomposition.

Main results

• TauCeti.quotientStabilizerEquivAlgHomSimpleField: the quotient of the normal-closure Galois group by a root stabilizer is the set of embeddings of the simple field.
• TauCeti.quotientGalStabilizerEquivAlgHomSimpleField: the corresponding quotient of the polynomial Galois group indexes those embeddings.
• TauCeti.quotientStabilizerEquivAlgHomSimpleField_smul: this equivalence respects the Galois action by postcomposition.

noncomputable def TauCeti.quotientStabilizerEquivAlgHomSimpleField {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E))) : Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F) ⧸ MulAction.stabilizer Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F) ↑y ≃ (↥F⟮x⟯ →ₐ[F] ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E))

The cosets of the stabilizer of a root are in bijection with the F-embeddings of F⟮x⟯ into its normal closure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.quotientStabilizerEquivAlgHomSimpleField_mk_gen {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E))) (σ : Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F)) : ((quotientStabilizerEquivAlgHomSimpleField x y) ↑σ) (IntermediateField.AdjoinSimple.gen F x) = σ • ↑y

The embedding indexed by the coset of σ sends the generator to σ • y.

@[simp]

theorem TauCeti.quotientStabilizerEquivAlgHomSimpleField_smul {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E))) (σ : Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F)) (c : Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F) ⧸ MulAction.stabilizer Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F) ↑y) : (quotientStabilizerEquivAlgHomSimpleField x y) (σ • c) = σ • (quotientStabilizerEquivAlgHomSimpleField x y) c

The coset-to-embedding correspondence intertwines the Galois action on cosets with postcomposition on embeddings.

noncomputable def TauCeti.quotientGalStabilizerEquivAlgHomSimpleField {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)) : (minpoly F x).Gal ⧸ MulAction.stabilizer (minpoly F x).Gal y ≃ (↥F⟮x⟯ →ₐ[F] ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E))

Cosets in the polynomial Galois group of a root stabilizer index the embeddings of the simple field into its normal closure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.quotientGalStabilizerEquivAlgHomSimpleField_mk_gen {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)) (σ : (minpoly F x).Gal) : ((quotientGalStabilizerEquivAlgHomSimpleField x y) ↑σ) (IntermediateField.AdjoinSimple.gen F x) = (splittingFieldEquivNormalClosure x) (σ • ↑y)

A polynomial Galois coset represented by σ sends the generator to the image of y under σ, transported to the normal closure.

@[simp]

theorem TauCeti.quotientGalStabilizerEquivAlgHomSimpleField_smul {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)) (σ : (minpoly F x).Gal) (q : (minpoly F x).Gal ⧸ MulAction.stabilizer (minpoly F x).Gal y) : (quotientGalStabilizerEquivAlgHomSimpleField x y) (σ • q) = (galEquivNormalClosure x) σ • (quotientGalStabilizerEquivAlgHomSimpleField x y) q

The polynomial Galois coset-to-embedding equivalence respects postcomposition.