The eliminant for a ratio g(beta)/f'(beta). For f,g in F[t][z], coefficients are lifted into F[u][t], and z is eliminated from f and uf'-g. The resulting polynomial has outer t-degree at most (2deg_z(f)-1) times the coefficient t-degree bound.

noncomputable def CCDN.residueParameterLift {F : Type u_1} [CommRing F] : Polynomial F →+* Polynomial (Polynomial F)

The embedding F[t] → F[u][t] of polynomials in t as polynomials with constant coefficients in the new parameter u.

Equations

• CCDN.residueParameterLift = Polynomial.mapRingHom Polynomial.C

noncomputable def CCDN.residueParameterZero {F : Type u_1} [CommRing F] : Polynomial (Polynomial F) →+* Polynomial F

The specialization F[u][t] → F[t] at u = 0.

Equations

• CCDN.residueParameterZero = Polynomial.mapRingHom (Polynomial.evalRingHom 0)

@[simp]

theorem CCDN.residueParameterZero_lift {F : Type u_1} [CommRing F] (a : Polynomial F) : residueParameterZero (residueParameterLift a) = a

Specializing u = 0 after lifting a polynomial in t to F[u][t] recovers it.

@[simp]

theorem CCDN.residueParameterZero_map_lift {F : Type u_1} [CommRing F] (f : Polynomial (Polynomial F)) : Polynomial.map residueParameterZero (Polynomial.map residueParameterLift f) = f

Applying residueParameterLift and then residueParameterZero to the coefficients of a polynomial over F[t] recovers it.

noncomputable def CCDN.residueEliminationEquation {F : Type u_1} [CommRing F] (f g : Polynomial (Polynomial F)) : Polynomial (Polynomial (Polynomial F))

The polynomial u · ∂f/∂z - g in z, with coefficients in F[u][t], whose common roots with f are the values u = g(β) / f'(β).

Equations

• CCDN.residueEliminationEquation f g = Polynomial.C (Polynomial.C Polynomial.X) * Polynomial.derivative (Polynomial.map CCDN.residueParameterLift f) - Polynomial.map CCDN.residueParameterLift g

noncomputable def CCDN.residueEliminant {F : Type u_1} [CommRing F] (f g : Polynomial (Polynomial F)) : Polynomial (Polynomial F)

The resultant in z of f and u · ∂f/∂z - g, a polynomial in t with coefficients in F[u] that vanishes at every ratio u = g(β) / f'(β) at a simple root β of f.

Equations

• CCDN.residueEliminant f g = (Polynomial.map CCDN.residueParameterLift f).resultant (CCDN.residueEliminationEquation f g) f.natDegree (f.natDegree - 1)

@[simp]

theorem CCDN.residueEliminationEquation_zero {F : Type u_1} [CommRing F] (f g : Polynomial (Polynomial F)) : Polynomial.map residueParameterZero (residueEliminationEquation f g) = -g

At u = 0, residueEliminationEquation f g specializes to -g.

theorem CCDN.residueEliminationEquation_natDegree_le {F : Type u_1} [CommRing F] (f g : Polynomial (Polynomial F)) (hg : g.natDegree < f.natDegree) : (residueEliminationEquation f g).natDegree ≤ f.natDegree - 1

If g has smaller z-degree than f, then residueEliminationEquation f g has z-degree at most deg_z f - 1.

theorem CCDN.residueEliminant_natDegree_le {F : Type u_1} [CommRing F] (f g : Polynomial (Polynomial F)) (D : ℕ) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ D) (hg : ∀ (i : ℕ), (g.coeff i).natDegree ≤ D) : (residueEliminant f g).natDegree ≤ (f.natDegree + (f.natDegree - 1)) * D

If all coefficients of f and g have t-degree at most D, then the residue eliminant has t-degree at most (2 deg_z f - 1) · D.

theorem CCDN.residueEliminant_ne_zero {F : Type u_1} [Field F] (f g : Polynomial (Polynomial F)) (hf : Irreducible (Polynomial.map (algebraMap (Polynomial F) (RatFunc F)) f)) (hg : g ≠ 0) (hdeg : g.natDegree < f.natDegree) : residueEliminant f g ≠ 0

The eliminant is nonzero: specializing u=0 gives the nonzero resultant of f and -g over F(t).