The parity character of a polynomial Galois group

Polynomial.Gal.sign p records the sign of the permutation of the distinct roots induced by a Galois automorphism. It is defined using the splitting field, but can be computed in any splitting extension and with any numbering of the roots. Its kernel is the even part of the root action; the character is trivial precisely when the Galois image lies in the alternating group.

No separability, irreducibility, monicity or characteristic assumption is needed. For an inseparable polynomial this is the parity of the action on its distinct roots, not an action on p.natDegree points. In particular, the integer-valued character remains meaningful in characteristic two, even though the discriminant test does not. For a separable quadratic, for instance, the character is trivial exactly when the quadratic has a root in the base field, in every characteristic.

The construction uses Mathlib's Polynomial.Gal.galActionHom and Equiv.Perm.sign; independence of the splitting extension uses Polynomial.Gal.galActionHom_eq_permCongr.

noncomputable def Polynomial.Gal.sign {F : Type u} [Field F] (p : Polynomial F) : p.Gal →* ℤˣ

The parity character of the action of p.Gal on the distinct roots of p in its splitting field. It takes values in ℤˣ, independently of the characteristic of the base field.

theorem Polynomial.Gal.sign_def {F : Type u} [Field F] (p : Polynomial F) : sign p = Equiv.Perm.sign.comp (galActionHom p p.SplittingField)

The parity character is the sign composed with the root action in the splitting field.

@[simp]

theorem Polynomial.Gal.sign_galActionHom {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] (g : p.Gal) : Equiv.Perm.sign ((galActionHom p E) g) = (sign p) g

The sign of a Galois automorphism can be read in any extension in which the polynomial splits. Thus the character does not depend on the choice of splitting extension.

@[simp]

theorem Polynomial.Gal.sign_comp_galActionHom {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] : Equiv.Perm.sign.comp (galActionHom p E) = sign p

Composing the root action in any splitting extension with the permutation sign gives the intrinsic parity character.

theorem Polynomial.Gal.ker_sign {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] : (sign p).ker = Subgroup.comap (galActionHom p E) (alternatingGroup ↑(p.rootSet E))

The kernel of the parity character consists of the automorphisms whose root permutations are even, computed in any splitting extension.

theorem Polynomial.Gal.sign_eq_one_iff_range_le_alternatingGroup {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] : sign p = 1 ↔ (galActionHom p E).range ≤ alternatingGroup ↑(p.rootSet E)

The parity character is trivial exactly when the Galois image consists of even permutations of the roots. No separability or characteristic restriction is needed for this characterization.

Quadratics

theorem Polynomial.Gal.range_le_alternatingGroup_iff_exists_isRoot_of_natDegree_eq_two {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] (hsep : p.Separable) (hdeg : p.natDegree = 2) : (galActionHom p E).range ≤ alternatingGroup ↑(p.rootSet E) ↔ ∃ (x : F), p.IsRoot x

The Galois image of a separable quadratic is even exactly when the quadratic has a root in the base field. The alternating group on two roots is trivial, so the image is even exactly when the Galois group is trivial, that is when the quadratic splits over the base field.

This holds in every characteristic. Away from characteristic 2, combined with the quadratic formula Polynomial.isSquare_discr_iff_exists_isRoot_of_degree_eq_two, it recovers the discriminant test Polynomial.Separable.isSquare_discr_iff_range_le_alternatingGroup for quadratics independently of the root-difference product. In characteristic 2 the separable quadratic X ^ 2 + X + 1 over ZMod 2 has no root, so its image is odd, while its discriminant is a square by Polynomial.isSquare_discr_of_char_two.

theorem Polynomial.Gal.sign_eq_one_iff_exists_isRoot_of_natDegree_eq_two {F : Type u} [Field F] (p : Polynomial F) (hsep : p.Separable) (hdeg : p.natDegree = 2) : sign p = 1 ↔ ∃ (x : F), p.IsRoot x

The parity character of a separable quadratic is trivial exactly when the quadratic has a root in the base field, in every characteristic. This is Polynomial.Gal.range_le_alternatingGroup_iff_exists_isRoot_of_natDegree_eq_two read in the splitting field.