Tschirnhaus transforms

Let f and T be polynomials over a commutative ring R. The Tschirnhaus transform of f by T is the polynomial whose roots are the values T(α) at the roots α of f, counted with multiplicity. It is defined on the coefficient side, as the resultant in X of f(X) and Y - T(X),

tschirnhausPolynomial f T = Res_X (f(X), Y - T(X)),

For monic f, it commutes with every base change R →+* S: the transform of a monic integral polynomial over ℚ is the image of its transform over ℤ, and the transform modulo p is its reduction. For arbitrary f, degree-dropping specialization need not preserve this resultant.

T is admissible for f over a field K when it separates the roots of f, that is, when a ↦ T(a) is injective on the roots of f in its splitting field. Admissibility does not depend on the field in which the roots are taken. For nonzero f over a field, the transform is separable exactly when f is separable and T is admissible. Admissible transforms are the classical remedy for a resolvent whose specialization at f is not separable: the resolvent is recomputed at the transform, whose roots are in bijection with those of f.

Main definitions

• Polynomial.tschirnhausPolynomial f T: the Tschirnhaus transform of f by T.
• Polynomial.TschirnhausAdmissible f T: T separates the roots of f.

Main results

• Polynomial.map_tschirnhausPolynomial: for monic f, the transform commutes with base change.
• Polynomial.map_tschirnhausPolynomial_of_injective: the same holds for any f under an injective base change.
• Polynomial.tschirnhausPolynomial_eq_prod_roots: over a domain in which monic f splits, the transform is ∏ (X - T(α)) over the roots α of f.
• Polynomial.tschirnhausPolynomial_eq_C_mul_prod_roots: the corresponding formula for any splitting polynomial over a domain, including its leading coefficient factor.
• Polynomial.ne_zero_tschirnhausPolynomial_field: the transform of any nonzero field polynomial is nonzero.
• Polynomial.monic_tschirnhausPolynomial, Polynomial.natDegree_tschirnhausPolynomial: the transform of a monic polynomial is monic of the same degree, over any commutative ring.
• Polynomial.aroots_tschirnhausPolynomial, Polynomial.rootSet_tschirnhausPolynomial: the roots of the transform are the values of T at the roots of f. The _field variants cover arbitrary field polynomials in splitting domains, including f = 0.
• Polynomial.isRoot_tschirnhausPolynomial: over a domain, T(α) is a root of the transform whenever α is a root of the nonzero polynomial f.
• Polynomial.Monic.tschirnhausRootMap, Polynomial.tschirnhausRootMap: the resulting map α ↦ T(α) from the roots of f to the roots of its transform, for monic f over a domain and for any field polynomial in a domain; it is surjective whenever f splits.
• Polynomial.separable_tschirnhausPolynomial_iff: the transform is separable if and only if f is separable and T is admissible.
• Polynomial.TschirnhausAdmissible.bijOn_rootSet: an admissible T maps the roots of f bijectively onto the roots of the transform.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, GTM 138, §6.3, where Tschirnhausen transformations are used to make a resolvent squarefree.

noncomputable def Polynomial.tschirnhausPolynomial {R : Type u_1} [CommRing R] (f T : Polynomial R) : Polynomial R

The Tschirnhaus transform of f by T: the resultant in X of f(X) and Y - T(X), as a polynomial in Y. When f is monic and splits, its roots are the values T(α) at the roots α of f, counted with multiplicity (Polynomial.tschirnhausPolynomial_eq_prod_roots).

Equations

• f.tschirnhausPolynomial T = (Polynomial.map Polynomial.C f).resultant (Polynomial.C Polynomial.X - Polynomial.map Polynomial.C T)

theorem Polynomial.tschirnhausPolynomial_def {R : Type u_1} [CommRing R] (f T : Polynomial R) : f.tschirnhausPolynomial T = (map C f).resultant (C X - map C T)

theorem Polynomial.tschirnhausPolynomial_eq_resultant {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) (T : Polynomial R) {n : ℕ} (hn : T.natDegree ≤ n) : f.tschirnhausPolynomial T = (map C f).resultant (C X - map C T) f.natDegree n

For monic f, the resultant defining the Tschirnhaus transform may be computed with any valid bound n on the degree of T.

@[simp]

theorem Polynomial.map_tschirnhausPolynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : Polynomial R} (hf : f.Monic) (T : Polynomial R) (φ : R →+* S) : map φ (f.tschirnhausPolynomial T) = (map φ f).tschirnhausPolynomial (map φ T)

Base change. For monic f, the Tschirnhaus transform commutes with every ring morphism. No hypothesis on T is needed, although its degree may drop.

@[simp]

theorem Polynomial.map_tschirnhausPolynomial_of_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f T : Polynomial R) (φ : R →+* S) (hφ : Function.Injective ⇑φ) : map φ (f.tschirnhausPolynomial T) = (map φ f).tschirnhausPolynomial (map φ T)

The Tschirnhaus transform commutes with an injective base change, without requiring f to be monic.

theorem Polynomial.tschirnhausPolynomial_eq_C_mul_prod_roots {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hs : f.Splits) (T : Polynomial R) : f.tschirnhausPolynomial T = C (f.leadingCoeff ^ (C X - map C T).natDegree) * (Multiset.map (fun (b : R) => X - C b) (Multiset.map (fun (x : R) => eval x T) f.roots)).prod

The root-product formula. Over a domain in which f splits, its Tschirnhaus transform is its leading coefficient raised to the degree in X of Y - T(X), times the product of X - T(α) over the roots α of f, counted with multiplicity.

theorem Polynomial.tschirnhausPolynomial_eq_prod_roots {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hf : f.Monic) (hs : f.Splits) (T : Polynomial R) : f.tschirnhausPolynomial T = (Multiset.map (fun (b : R) => X - C b) (Multiset.map (fun (x : R) => eval x T) f.roots)).prod

The monic root-product formula. Over a domain in which the monic polynomial f splits, the Tschirnhaus transform of f by T is ∏ (X - T(α)).

@[simp]

theorem Polynomial.roots_tschirnhausPolynomial {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hs : f.Splits) (T : Polynomial R) : (f.tschirnhausPolynomial T).roots = Multiset.map (fun (x : R) => eval x T) f.roots

For a polynomial over a domain that splits, the roots of its Tschirnhaus transform are the values of T at its roots, counted with multiplicity. Both sides are empty when f = 0.

theorem Polynomial.isRoot_tschirnhausPolynomial {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hf : f ≠ 0) {a : R} (ha : f.IsRoot a) (T : Polynomial R) : (f.tschirnhausPolynomial T).IsRoot (eval a T)

For a nonzero polynomial over a domain, the value of T at any root of f is a root of the Tschirnhaus transform; no splitting hypothesis is needed.

theorem Polynomial.splits_tschirnhausPolynomial {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hs : f.Splits) (T : Polynomial R) : (f.tschirnhausPolynomial T).Splits

The Tschirnhaus transform splits in every domain in which f splits.

theorem Polynomial.monic_tschirnhausPolynomial {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) (T : Polynomial R) : (f.tschirnhausPolynomial T).Monic

The Tschirnhaus transform of a monic polynomial is monic, over any commutative ring.

@[simp]

theorem Polynomial.natDegree_tschirnhausPolynomial {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) (T : Polynomial R) : (f.tschirnhausPolynomial T).natDegree = f.natDegree

The Tschirnhaus transform of a monic polynomial has the same degree, whatever the degree of T, over any commutative ring.

@[simp]

theorem Polynomial.tschirnhausPolynomial_X {R : Type u_1} [CommRing R] (f : Polynomial R) : f.tschirnhausPolynomial X = f

The Tschirnhaus transform by X is the identity.

@[simp]

theorem Polynomial.tschirnhausPolynomial_C {R : Type u_1} [CommRing R] (f : Polynomial R) (c : R) : f.tschirnhausPolynomial (C c) = (X - C c) ^ f.natDegree

The Tschirnhaus transform by a constant c collapses every root to c.

@[simp]

theorem Polynomial.aroots_tschirnhausPolynomial {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (f.tschirnhausPolynomial T).aroots L = Multiset.map (fun (a : L) => (aeval a) T) (f.aroots L)

If the monic polynomial f splits in the domain L, then the roots in L of the Tschirnhaus transform are the values of T at the roots of f in L, counted with multiplicity.

@[simp]

theorem Polynomial.rootSet_tschirnhausPolynomial {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (f.tschirnhausPolynomial T).rootSet L = (fun (a : L) => (aeval a) T) '' f.rootSet L

If the monic polynomial f splits in the domain L, then the roots in L of the Tschirnhaus transform are the images under T of the roots of f in L.

noncomputable def Polynomial.Monic.tschirnhausRootMap {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (T : Polynomial K) : ↑(f.rootSet L) → ↑((f.tschirnhausPolynomial T).rootSet L)

The map from the roots of a monic polynomial f to the roots of its Tschirnhaus transform, sending α to T(α), in a domain L.

Equations

• hf.tschirnhausRootMap T = Set.MapsTo.restrict (fun (a : L) => (Polynomial.aeval a) T) (f.rootSet L) ((f.tschirnhausPolynomial T).rootSet L) ⋯

@[simp]

theorem Polynomial.Monic.coe_tschirnhausRootMap {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (T : Polynomial K) (x : ↑(f.rootSet L)) : ↑(hf.tschirnhausRootMap T x) = (aeval ↑x) T

theorem Polynomial.Monic.tschirnhausRootMap_surjective {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (hs : (Polynomial.map (algebraMap K L) f).Splits) (T : Polynomial K) : Function.Surjective (hf.tschirnhausRootMap T)

Every root of the Tschirnhaus transform of a monic polynomial is the image of a root of the original polynomial.

theorem Polynomial.splits_map_tschirnhausPolynomial {K : Type u_3} {L : Type u_4} [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hf : f.Monic) (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (map (algebraMap K L) (f.tschirnhausPolynomial T)).Splits

If a monic polynomial splits after a base change, then its Tschirnhaus transform splits after the same base change.

theorem Polynomial.ne_zero_tschirnhausPolynomial_field {K : Type u_3} [Field K] {f : Polynomial K} (hf : f ≠ 0) (T : Polynomial K) : f.tschirnhausPolynomial T ≠ 0

Over a field, the Tschirnhaus transform of a nonzero polynomial is nonzero.

@[simp]

theorem Polynomial.aroots_tschirnhausPolynomial_field {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (f.tschirnhausPolynomial T).aroots L = Multiset.map (fun (a : L) => (aeval a) T) (f.aroots L)

In any domain in which a field polynomial splits, the roots of its transform are the values of T at its roots, counted with multiplicity. Both sides are empty when f = 0.

@[simp]

theorem Polynomial.rootSet_tschirnhausPolynomial_field {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (f.tschirnhausPolynomial T).rootSet L = (fun (a : L) => (aeval a) T) '' f.rootSet L

The root set of the transform of a field polynomial is the image of the root set under T, in any domain in which f splits. Both sides are empty when f = 0.

theorem Polynomial.splits_map_tschirnhausPolynomial_field {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (map (algebraMap K L) (f.tschirnhausPolynomial T)).Splits

If a polynomial over a field splits after a base change to a domain, then its Tschirnhaus transform splits after the same base change.

noncomputable def Polynomial.tschirnhausRootMap {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] (f T : Polynomial K) : ↑(f.rootSet L) → ↑((f.tschirnhausPolynomial T).rootSet L)

The map from the roots of a field polynomial to the roots of its Tschirnhaus transform in a domain, sending α to T(α).

Equations

• f.tschirnhausRootMap T = Set.MapsTo.restrict (fun (a : L) => (Polynomial.aeval a) T) (f.rootSet L) ((f.tschirnhausPolynomial T).rootSet L) ⋯

@[simp]

theorem Polynomial.coe_tschirnhausRootMap {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] (f T : Polynomial K) (x : ↑(f.rootSet L)) : ↑(f.tschirnhausRootMap T x) = (aeval ↑x) T

theorem Polynomial.tschirnhausRootMap_surjective {K : Type u_3} [Field K] {L : Type u_4} [CommRing L] [IsDomain L] [Algebra K L] {f : Polynomial K} (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : Function.Surjective (f.tschirnhausRootMap T)

Every root in a splitting domain of the Tschirnhaus transform of a field polynomial is the image of a root of the original polynomial. For f = 0 the transform is 0 or 1, so both root sets are empty.

def Polynomial.TschirnhausAdmissible {K : Type u_3} [Field K] (f T : Polynomial K) : Prop

T is admissible for f, or separates the roots of f, when a ↦ T(a) is injective on the roots of f in its splitting field. By Polynomial.tschirnhausAdmissible_iff_injOn, the splitting field may be replaced by any field in which f splits.

Equations

• f.TschirnhausAdmissible T = Set.InjOn (fun (a : f.SplittingField) => (Polynomial.aeval a) T) (f.rootSet f.SplittingField)

theorem Polynomial.tschirnhausAdmissible_iff_injOn {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f T : Polynomial K} (hs : (map (algebraMap K L) f).Splits) : f.TschirnhausAdmissible T ↔ Set.InjOn (fun (a : L) => (aeval a) T) (f.rootSet L)

Admissibility may be tested in any field in which f splits.

@[simp]

theorem Polynomial.tschirnhausAdmissible_X {K : Type u_3} [Field K] (f : Polynomial K) : f.TschirnhausAdmissible X

The Tschirnhaus transform by X is admissible.

theorem Polynomial.separable_tschirnhausPolynomial_iff_of_splits {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f : Polynomial K} (hf : f ≠ 0) (hs : (map (algebraMap K L) f).Splits) (T : Polynomial K) : (f.tschirnhausPolynomial T).Separable ↔ f.Separable ∧ Set.InjOn (fun (a : L) => (aeval a) T) (f.rootSet L)

If the nonzero polynomial f splits in L, then its Tschirnhaus transform by T is separable if and only if f is separable and T is injective on the roots of f in L.

theorem Polynomial.separable_tschirnhausPolynomial_iff {K : Type u_3} [Field K] {f : Polynomial K} (hf : f ≠ 0) (T : Polynomial K) : (f.tschirnhausPolynomial T).Separable ↔ f.Separable ∧ f.TschirnhausAdmissible T

Separability of the Tschirnhaus transform. For nonzero f, the Tschirnhaus transform by T is separable if and only if f is separable and T is admissible for f.

theorem Polynomial.TschirnhausAdmissible.bijOn_rootSet {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f T : Polynomial K} (hT : f.TschirnhausAdmissible T) (hs : (map (algebraMap K L) f).Splits) : Set.BijOn (fun (a : L) => (aeval a) T) (f.rootSet L) ((f.tschirnhausPolynomial T).rootSet L)

The root sets correspond. If T is admissible for a polynomial f that splits in L, then a ↦ T(a) maps the roots of f in L bijectively onto the roots of the Tschirnhaus transform in L. Both root sets are empty when f = 0.

noncomputable def Polynomial.TschirnhausAdmissible.rootSetEquiv {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f T : Polynomial K} (hT : f.TschirnhausAdmissible T) (hs : (map (algebraMap K L) f).Splits) : ↑(f.rootSet L) ≃ ↑((f.tschirnhausPolynomial T).rootSet L)

The canonical equivalence from the roots of f to the roots of an admissible Tschirnhaus transform, sending α to T(α).

Equations

• hT.rootSetEquiv hs = Equiv.ofBijective (Set.MapsTo.restrict (fun (a : L) => (Polynomial.aeval a) T) (f.rootSet L) ((f.tschirnhausPolynomial T).rootSet L) ⋯) ⋯

@[simp]

theorem Polynomial.TschirnhausAdmissible.coe_rootSetEquiv_apply {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f T : Polynomial K} (hT : f.TschirnhausAdmissible T) (hs : (map (algebraMap K L) f).Splits) (x : ↑(f.rootSet L)) : ↑((hT.rootSetEquiv hs) x) = (aeval ↑x) T

@[simp]

theorem Polynomial.TschirnhausAdmissible.aeval_coe_rootSetEquiv_symm_apply {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] {f T : Polynomial K} (hT : f.TschirnhausAdmissible T) (hs : (map (algebraMap K L) f).Splits) (y : ↑((f.tschirnhausPolynomial T).rootSet L)) : (aeval ↑((hT.rootSetEquiv hs).symm y)) T = ↑y

Applying T to the inverse image under the canonical root equivalence recovers the root.