Documentation

TauCeti.FieldTheory.GaloisGroups.Tschirnhaus

Tschirnhaus transforms and the Galois group #

A Tschirnhaus transform Polynomial.tschirnhausPolynomial f T replaces the roots α of f by the values T(α). The coefficient-side construction and the root correspondence are developed in TauCeti/RingTheory/Polynomial/Tschirnhaus.lean. This file shows that for a separable f an admissible transform — one that separates the roots of f — changes neither the splitting field nor the Galois group.

Separability of f is assumed by the two splitting-field results. The Galois correspondence enters in one place only, the splitting-field argument Polynomial.TschirnhausAdmissible.isSplittingField, which computes the fixing subgroup of the field generated by the values T(α). The conjugacy of the Galois images needs only that the transform is admissible.

For any f and any field extension E in which f splits, the roots of the transform are exactly the values of T at the roots of f, with multiplicity, so the transform splits in E as well. Consequently restriction along Mathlib's chosen embedding of splitting fields gives a surjection from the Galois group of f onto the Galois group of any Tschirnhaus transform. On roots, this quotient map intertwines the polynomial map α ↦ T(α). These declarations specialize Polynomial.Gal.restrict, Polynomial.Gal.restrict_surjective, and Polynomial.Gal.galActionHom_restrict from Mathlib's Mathlib.FieldTheory.PolynomialGaloisGroup. Admissibility is Polynomial.TschirnhausAdmissible f T: injectivity of α ↦ T(α) on the root set of f in its splitting field. Under it, a separable f has a separable transform and each splitting field of f is a splitting field of the transform. For any f, the Galois groups are isomorphic and their images inside the permutations of their respective root sets are conjugate along α ↦ T(α). When f = 0, the root sets are empty and both Galois groups are trivial.

That last statement is what carries information back: a constraint on the Galois image of the transform — typically an upper bound read off a resolvent that became separable after the substitution — is a constraint on the Galois image of f.

Main results #

References #

source
theorem Polynomial.TschirnhausAdmissible.eqOn_rootSet {F : Type u_1} [Field F] {f T : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] (h : f.TschirnhausAdmissible T) (hs : (map (algebraMap F E) f).Splits) {φ ψ : Gal(E/F)} (hφψ : Set.EqOn (⇑φ) (⇑ψ) ((f.tschirnhausPolynomial T).rootSet E)) :
Set.EqOn (⇑φ) (⇑ψ) (f.rootSet E)

Automorphisms that agree on the roots of an admissible Tschirnhaus transform agree on the roots of the original polynomial.

source
theorem Polynomial.TschirnhausAdmissible.algEquiv_ext {F : Type u_1} [Field F] {f T : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] [IsSplittingField F E f] (h : f.TschirnhausAdmissible T) {φ ψ : Gal(E/F)} (hφψ : ∀ x ∈ f.rootSet E, φ ((aeval x) T) = ψ ((aeval x) T)) :
φ = ψ

Two automorphisms of a splitting field of f are equal if they agree on every T(α), when T is admissible for f.

source
noncomputable def Polynomial.Gal.restrictTschirnhaus {F : Type u_1} [Field F] (f T : Polynomial F) :
f.Gal →* (f.tschirnhausPolynomial T).Gal

Restriction from the Galois group of a polynomial to that of a Tschirnhaus transform.

The transform splits in the splitting field of the original polynomial, so restriction along the embedding of splitting fields chosen by Polynomial.Gal.restrict defines this homomorphism without an admissibility hypothesis.

Equations
Instances For
    source
    theorem Polynomial.Gal.restrictTschirnhaus_surjective {F : Type u_1} [Field F] (f T : Polynomial F) :
    Function.Surjective ⇑(restrictTschirnhaus f T)

    The Galois group of a Tschirnhaus transform is a quotient of the Galois group of the original polynomial. No separation hypothesis on the transformed roots is needed.

    source
    noncomputable def Polynomial.Gal.tschirnhausActionHom {F : Type u_1} [Field F] (f T : Polynomial F) :
    f.Gal →* Equiv.Perm ↑((f.tschirnhausPolynomial T).rootSet f.SplittingField)

    The action of the original Galois group on the roots of a Tschirnhaus transform, obtained by restricting to the transform's Galois group.

    Equations
    Instances For
      source
      @[simp]
      theorem Polynomial.Gal.coe_tschirnhausActionHom_apply {F : Type u_1} [Field F] (f T : Polynomial F) (g : f.Gal) (y : ↑((f.tschirnhausPolynomial T).rootSet f.SplittingField)) :
      ↑(((tschirnhausActionHom f T) g) y) = g ↑y

      The action induced by restriction on each transformed root is the original splitting-field automorphism.

      source
      @[simp]
      theorem Polynomial.Gal.tschirnhausActionHom_apply_rootMap {F : Type u_1} [Field F] (f T : Polynomial F) (g : f.Gal) (x : ↑(f.rootSet f.SplittingField)) :
      ((tschirnhausActionHom f T) g) (f.tschirnhausRootMap T x) = f.tschirnhausRootMap T ⟨g ↑x, ⋯⟩

      The root map α ↦ T(α) is equivariant for restriction to the Galois group of the Tschirnhaus transform.

      source
      theorem Polynomial.TschirnhausAdmissible.isSplittingField {F : Type u_1} [Field F] {f T : Polynomial F} {L : Type u_2} [Field L] [Algebra F L] [IsSplittingField F L f] (h : f.TschirnhausAdmissible T) (hsep : f.Separable) :
      IsSplittingField F L (f.tschirnhausPolynomial T)

      Every splitting field of f is a splitting field of an admissible transform. For a separable f and an admissible T, the transform splits in any splitting field L of f and its roots generate L over F.

      source
      theorem Polynomial.TschirnhausAdmissible.nonempty_algEquiv_splittingField {F : Type u_1} [Field F] {f T : Polynomial F} (h : f.TschirnhausAdmissible T) (hsep : f.Separable) :
      Nonempty (f.SplittingField ≃ₐ[F] (f.tschirnhausPolynomial T).SplittingField)

      The splitting field of f is a splitting field of an admissible transform, so the two splitting fields agree up to an F-algebra equivalence.

      source
      theorem Polynomial.TschirnhausAdmissible.nonempty_mulEquiv_gal {F : Type u_1} [Field F] {f T : Polynomial F} (h : f.TschirnhausAdmissible T) :
      Nonempty ((f.tschirnhausPolynomial T).Gal ≃* f.Gal)

      An admissible Tschirnhaus transform has the same Galois group as the original polynomial. This includes f = 0, when both Galois groups are trivial.

      source
      theorem Polynomial.TschirnhausAdmissible.galActionHom_restrict_rootSetEquiv {F : Type u_1} [Field F] {f T : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] (h : f.TschirnhausAdmissible T) [hfsp : Fact (map (algebraMap F E) f).Splits] [Fact (map (algebraMap F E) (f.tschirnhausPolynomial T)).Splits] (φ : Gal(E/F)) (x : ↑(f.rootSet E)) :
      ((Gal.galActionHom (f.tschirnhausPolynomial T) E) ((Gal.restrict (f.tschirnhausPolynomial T) E) φ)) ((h.rootSetEquiv ⋯) x) = (h.rootSetEquiv ⋯) (((Gal.galActionHom f E) ((Gal.restrict f E) φ)) x)

      The canonical root-set equivalence for an admissible Tschirnhaus transform intertwines the root actions induced by every automorphism of a common splitting extension.

      source
      theorem Polynomial.TschirnhausAdmissible.range_galActionHom_eq_map_rootSetEquiv {F : Type u_1} [Field F] {f T : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] [Normal F E] (h : f.TschirnhausAdmissible T) [hfsp : Fact (map (algebraMap F E) f).Splits] [Fact (map (algebraMap F E) (f.tschirnhausPolynomial T)).Splits] :
      (Gal.galActionHom (f.tschirnhausPolynomial T) E).range = Subgroup.map (h.rootSetEquiv ⋯).permCongrHom.toMonoidHom (Gal.galActionHom f E).range

      The Galois images of f and of an admissible transform are conjugate. In any normal extension where both polynomials split, they are conjugate along the canonical root equivalence α ↦ T(α).

      source
      theorem Polynomial.TschirnhausAdmissible.map_range_galActionHom_tschirnhausPolynomial {F : Type u_1} [Field F] {f T : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] [Normal F E] (h : f.TschirnhausAdmissible T) [hfsp : Fact (map (algebraMap F E) f).Splits] [Fact (map (algebraMap F E) (f.tschirnhausPolynomial T)).Splits] {ι : Type u_3} (e : ↑(f.rootSet E) ≃ ι) :
      Subgroup.map (↑((h.rootSetEquiv ⋯).symm.trans e).permCongrHom) (Gal.galActionHom (f.tschirnhausPolynomial T) E).range = Subgroup.map (↑e.permCongrHom) (Gal.galActionHom f E).range

      The Galois images agree once the roots are numbered compatibly. Number the roots of f by e, and the roots of an admissible transform by T(α) ↦ e α. Read through these numberings, the Galois images of f and of the transform are the same subgroup of Equiv.Perm ι. A statement about the image of the transform read through some numbering, such as the subgroup bound that a resolvent of the transform provides, is therefore a statement about the image of f.