Translating the variable, and depressed quartics

Replacing f(X) by f(X + t) for a constant t of the base field moves every root of f by -t. Since t is fixed by every automorphism over the base field, this changes neither the splitting field nor the Galois action on the roots: the root sets correspond by x ↦ x + t, equivariantly for every automorphism, and so the two Galois images are the same permutation group read through that bijection. In particular f(X + t) and f carry the same transitive-group label.

The classical use is depression. Away from characteristic 2 the substitution X ↦ X - a/4 carries the quartic X⁴ + aX³ + bX² + cX + d to a quartic X⁴ + pX² + qX + r without cubic term, with

p = b - 6s², q = c - 2bs + 8s³, r = d - cs + bs² - 3s⁴,   s = a/4.

So the label of any quartic is the label of a depressed one, which is the form in which the resolvent cubic TauCeti.resolventCubic is written.

Main results

• Polynomial.isSplittingField_comp_X_add_C_iff: f(X + t) and f have the same splitting fields.
• Polynomial.galActionHom_restrict_rootSetCompXAddCEquiv: the bijection Polynomial.rootSetCompXAddCEquiv of root sets is equivariant for every automorphism of a normal extension in which f splits.
• Polynomial.map_range_galActionHom_comp_X_add_C: the Galois images of f(X + t) and f correspond along that bijection.
• TauCeti.hasGaloisLabel_comp_X_add_C_iff: f(X + t) and f have the same label.
• TauCeti.quartic_comp_X_sub_C, TauCeti.hasGaloisLabel_quartic_iff_depressed: the depression of a quartic, and its invariance of the label.

References

• K. Conrad, Galois groups of cubics and quartics (not in characteristic 2), §1.

theorem Polynomial.splits_map_comp_X_add_C_iff {F : Type u_1} [Field F] {L : Type u_2} [Field L] [Algebra F L] {p : Polynomial F} {t : F} : (map (algebraMap F L) (p.comp (X + C t))).Splits ↔ (map (algebraMap F L) p).Splits

p(X + t) splits in an extension exactly when p does.

theorem Polynomial.isSplittingField_comp_X_add_C_iff {F : Type u_1} [Field F] {L : Type u_2} [Field L] [Algebra F L] {p : Polynomial F} {t : F} : IsSplittingField F L (p.comp (X + C t)) ↔ IsSplittingField F L p

p(X + t) and p have the same splitting fields: the roots of one are the roots of the other moved by an element of the base field, so they generate the same subalgebra.

theorem Polynomial.galActionHom_restrict_rootSetCompXAddCEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (p : Polynomial F) (t : F) [Fact (map (algebraMap F E) p).Splits] [Fact (map (algebraMap F E) (p.comp (X + C t))).Splits] (ϕ : Gal(E/F)) (x : ↑((p.comp (X + C t)).rootSet E)) : ((Gal.galActionHom p E) ((Gal.restrict p E) ϕ)) ((p.rootSetCompXAddCEquiv t E) x) = (p.rootSetCompXAddCEquiv t E) (((Gal.galActionHom (p.comp (X + C t)) E) ((Gal.restrict (p.comp (X + C t)) E) ϕ)) x)

The translation of roots is Galois-equivariant. For an automorphism ϕ of an extension in which p splits, moving a root of p(X + t) by t and then applying ϕ agrees with applying ϕ and then moving by t, since ϕ fixes t.

theorem Polynomial.map_range_galActionHom_comp_X_add_C {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (p : Polynomial F) (t : F) [Normal F E] [Fact (map (algebraMap F E) p).Splits] [Fact (map (algebraMap F E) (p.comp (X + C t))).Splits] : Subgroup.map (p.rootSetCompXAddCEquiv t E).permCongrHom.toMonoidHom (Gal.galActionHom (p.comp (X + C t)) E).range = (Gal.galActionHom p E).range

The Galois images of p(X + t) and p correspond. Read through the bijection x ↦ x + t of root sets, the permutations of the roots of p(X + t) induced by its Galois group are exactly those of the roots of p induced by the Galois group of p. The roots may be taken in any normal extension in which p splits.

@[simp]

theorem TauCeti.hasGaloisLabel_comp_X_add_C_iff {F : Type u_1} [Field F] {f : Polynomial F} {t : F} {n : ℕ} {j : TransitiveGroupIndex n} : HasGaloisLabel (f.comp (Polynomial.X + Polynomial.C t)) j ↔ HasGaloisLabel f j

Translating the variable does not change the label. f(X + t) carries the transitive-group label j exactly when f does.

theorem TauCeti.quartic_comp_X_sub_C {R : Type u_2} [CommRing R] (s b c d : R) : (Polynomial.X ^ 4 + Polynomial.C (4 * s) * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).comp (Polynomial.X - Polynomial.C s) = Polynomial.X ^ 4 + Polynomial.C (b - 6 * s ^ 2) * Polynomial.X ^ 2 + Polynomial.C (c - 2 * b * s + 8 * s ^ 3) * Polynomial.X + Polynomial.C (d - c * s + b * s ^ 2 - 3 * s ^ 4)

The depression of a quartic. Substituting X - s into X⁴ + 4s X³ + bX² + cX + d removes the cubic term. The identity holds over every commutative ring.

theorem TauCeti.hasGaloisLabel_quartic_iff_depressed {F : Type u_1} [Field F] (hchar : ringChar F ≠ 2) (a b c d : F) {j : TransitiveGroupIndex 4} : HasGaloisLabel (Polynomial.X ^ 4 + Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) j ↔ HasGaloisLabel (Polynomial.X ^ 4 + Polynomial.C (b - 6 * (a / 4) ^ 2) * Polynomial.X ^ 2 + Polynomial.C (c - 2 * b * (a / 4) + 8 * (a / 4) ^ 3) * Polynomial.X + Polynomial.C (d - c * (a / 4) + b * (a / 4) ^ 2 - 3 * (a / 4) ^ 4)) j

Depression does not change the label. Away from characteristic 2, the quartic X⁴ + aX³ + bX² + cX + d carries the same label as the depressed quartic X⁴ + pX² + qX + r obtained from it by the substitution X ↦ X - a/4.