Discriminants under changes of root coordinate

Translation of the root coordinate preserves the discriminant. Reversal also preserves it when the constant coefficient is nonzero, so that reversal preserves degree. These identities allow reciprocal coordinates centered at a nonroot: the new leading coefficient is the value of the original polynomial at that center. In a polynomial family this is useful even when the original leading coefficient vanishes upon specialization. Reversal is taken at the formal degree before specialization; it must not be recomputed at a smaller fiber degree.

Combined with integral normalization, reversal at a nonroot a turns any polynomial into a monic polynomial over the same ring whose discriminant is that of the original polynomial times a power of its value at a.

The identities include repeated roots and constant polynomials. No separability or characteristic-zero hypothesis is needed.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (delineability).
• S. Lang, Algebra, third edition, Chapter IV, §8 (discriminants and root products).

@[simp]

theorem Polynomial.discr_comp_X_add_C {R : Type u_1} [CommRing R] (f : Polynomial R) (a : R) : (f.comp (X + C a)).discr = f.discr

Translating the root coordinate preserves the discriminant over any commutative ring.

@[simp]

theorem Polynomial.discr_reverse {R : Type u_1} [CommRing R] (f : Polynomial R) (h0 : f.coeff 0 ≠ 0) : f.reverse.discr = f.discr

Reversal preserves the discriminant when the constant coefficient is nonzero. The condition ensures that reversal preserves the degree; without it the statement can fail.

@[simp]

theorem Polynomial.discr_map_reverse {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : Polynomial R) (φ : R →+* S) (h0 : φ (f.coeff 0) ≠ 0) : (map φ f.reverse).discr = φ f.discr

Specializing a reversal taken at the formal degree preserves the formal discriminant whenever the specialized constant coefficient is nonzero. The original polynomial may drop degree under φ; the reversed polynomial retains its degree.

theorem Polynomial.natDegree_reverse_comp_X_add_C {R : Type u_1} [CommRing R] (f : Polynomial R) {a : R} (h : eval a f ≠ 0) : (f.comp (X + C a)).reverse.natDegree = f.natDegree

Translating the root coordinate to a nonroot a and reversing at the formal degree keeps the degree.

theorem Polynomial.leadingCoeff_reverse_comp_X_add_C {R : Type u_1} [CommRing R] (f : Polynomial R) {a : R} (h : eval a f ≠ 0) : (f.comp (X + C a)).reverse.leadingCoeff = eval a f

Translating the root coordinate to a nonroot a and reversing at the formal degree gives leading coefficient f.eval a.

theorem Polynomial.discr_integralNormalization_reverse_comp_X_add_C {R : Type u_1} [CommRing R] (f : Polynomial R) {a : R} (h : eval a f ≠ 0) : (f.comp (X + C a)).reverse.integralNormalization.discr = eval a f ^ ((f.natDegree - 1) * (f.natDegree - 2)) * f.discr

Normalized reciprocal coordinates centered at a nonroot a multiply the discriminant of a degree n polynomial by the (n - 1) * (n - 2) power of f.eval a. In a polynomial family, f.eval a can remain nonzero under a specialization that kills the leading coefficient of f; when that specialization lands in a field, such as ℝ, the factor becomes a unit, so this monic polynomial over the same ring carries the discriminant of f up to a unit factor there.