Blocks of a polynomial Galois action

For an irreducible separable polynomial, the blocks of the Galois action that contain a chosen root correspond contravariantly to the intermediate fields of the simple extension generated by that root. A block is sent to the field fixed by its setwise stabilizer; in the other direction, an intermediate field is sent to the orbit of the root under its fixing subgroup. Equivalently, that orbit consists of the roots of the root's minimal polynomial over the intermediate field.

The correspondence identifies primitivity of the root action with the absence of proper intermediate fields in the simple extension.

Main results

• TauCeti.rootBlockIntermediateFieldOrderIso: blocks containing a root are order anti-isomorphic to intermediate fields contained in the field generated by that root.
• TauCeti.coe_rootBlockIntermediateFieldOrderIso_symm_apply_eq_preimage_rootSet_minpoly: the block attached to an intermediate field is the set of roots of the corresponding minimal polynomial.
• TauCeti.isPreprimitive_iff_isAtom_adjoin_simple: the root action is primitive exactly when the generated simple extension is an atom in the lattice of intermediate fields.
• TauCeti.isPreprimitive_of_irreducible_of_separable_of_prime_natDegree: an irreducible separable polynomial of prime degree has a primitive root action.

References

• H. Wielandt, Finite Permutation Groups, Theorem 7.5
• J. D. Dixon and B. Mortimer, Permutation Groups, Section 1.5

noncomputable def TauCeti.rootBlockIntermediateFieldOrderIso {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) : MulAction.BlockMem p.Gal x ≃o (↑(Set.Iic F⟮↑x⟯))ᵒᵈ

Blocks containing a root correspond to intermediate fields of its simple extension.

The correspondence sends a block B to the field fixed by its setwise stabilizer. Its inverse sends an intermediate field E ⊆ F⟨x⟩ to the orbit of x under Gal(L/E), where L = p.SplittingField. The codomain is order-dual because larger blocks have larger stabilizers and hence smaller fixed fields.

Equations

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

@[simp]

theorem TauCeti.mem_rootBlockIntermediateFieldOrderIso_apply_iff {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) (B : MulAction.BlockMem p.Gal x) (y : p.SplittingField) : y ∈ ↑(OrderDual.ofDual ((rootBlockIntermediateFieldOrderIso hp hsep x) B)) ↔ ∀ g ∈ MulAction.stabilizer p.Gal ↑B, g • y = y

A block is sent to the field fixed by its setwise stabilizer: an element belongs to the corresponding intermediate field exactly when every element of the stabilizer fixes it.

theorem TauCeti.rootBlockIntermediateFieldOrderIso_apply_bot {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) : ↑(OrderDual.ofDual ((rootBlockIntermediateFieldOrderIso hp hsep x) ⊥)) = F⟮↑x⟯

The singleton block corresponds to the whole simple extension, confirming the orientation of rootBlockIntermediateFieldOrderIso.

theorem TauCeti.rootBlockIntermediateFieldOrderIso_apply_top {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) : ↑(OrderDual.ofDual ((rootBlockIntermediateFieldOrderIso hp hsep x) ⊤)) = ⊥

The block of all roots corresponds to the base field, confirming the orientation of rootBlockIntermediateFieldOrderIso.

@[simp]

theorem TauCeti.coe_rootBlockIntermediateFieldOrderIso_symm_apply {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) (E : ↑(Set.Iic F⟮↑x⟯)) : ↑((rootBlockIntermediateFieldOrderIso hp hsep x).symm (OrderDual.toDual E)) = MulAction.orbit (↥(fixingSubgroup p.Gal ↑↑E)) x

The underlying set of the block attached to an intermediate field is the orbit of the chosen root under the field's fixing subgroup.

theorem TauCeti.coe_rootBlockIntermediateFieldOrderIso_symm_apply_eq_preimage_rootSet_minpoly {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) (E : ↑(Set.Iic F⟮↑x⟯)) : ↑((rootBlockIntermediateFieldOrderIso hp hsep x).symm (OrderDual.toDual E)) = Subtype.val ⁻¹' (minpoly ↥↑E ↑x).rootSet p.SplittingField

The block attached to an intermediate field is the fibre, among the roots of p, of the minimal polynomial of the chosen root over that field.

theorem TauCeti.isPreprimitive_iff_isAtom_adjoin_simple {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (hdeg : 1 < p.natDegree) (x : ↑(p.rootSet p.SplittingField)) : MulAction.IsPreprimitive p.Gal ↑(p.rootSet p.SplittingField) ↔ IsAtom F⟮↑x⟯

The Galois action on the roots is primitive exactly when the simple extension generated by a root has no proper intermediate fields. The degree assumption excludes the one-point action, for which Mathlib's definition of primitivity is deliberately nontrivial.

theorem TauCeti.isPreprimitive_of_irreducible_of_separable_of_prime_natDegree {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (hprime : Nat.Prime p.natDegree) : MulAction.IsPreprimitive p.Gal ↑(p.rootSet p.SplittingField)

An irreducible separable polynomial of prime degree has a primitive Galois action on its roots.