Evaluation of the residue eliminant. The Sylvester Bezout identity proves its vanishing at every ratio g(beta)/f'(beta) at a simple root.

noncomputable def CCDN.residueParameterEval {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (t u : L) : Polynomial (Polynomial F) →+* L

The evaluation F[u][t] → L at u and t, for elements t, u of an F-algebra L.

Equations

• CCDN.residueParameterEval t u = Polynomial.eval₂RingHom (Polynomial.aeval u).toRingHom t

@[simp]

theorem CCDN.residueParameterEval_lift {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (t u : L) (a : Polynomial F) : (residueParameterEval t u) (residueParameterLift a) = (Polynomial.aeval t) a

Evaluating the lift of a polynomial a ∈ F[t] at (t, u) gives a(t).

@[simp]

theorem CCDN.residueParameterEval_C_X {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (t u : L) : (residueParameterEval t u) (Polynomial.C Polynomial.X) = u

The parameter u ∈ F[u][t] evaluates to u.

@[simp]

theorem CCDN.residueParameterEval_map_lift {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (t u : L) (f : Polynomial (Polynomial F)) : Polynomial.map (residueParameterEval t u) (Polynomial.map residueParameterLift f) = Polynomial.map (Polynomial.aeval t).toRingHom f

Applying residueParameterLift and then evaluation at (t, u) to the coefficients of a polynomial over F[t] is evaluating its coefficients at t.

theorem CCDN.residueEliminant_eval_ratio_eq_zero {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (t β : L) (f g : Polynomial (Polynomial F)) (hdeg : g.natDegree < f.natDegree) (hroot : Polynomial.eval β (Polynomial.map (Polynomial.aeval t).toRingHom f) = 0) (hsimple : Polynomial.eval β (Polynomial.derivative (Polynomial.map (Polynomial.aeval t).toRingHom f)) ≠ 0) : have u := Polynomial.eval β (Polynomial.map (Polynomial.aeval t).toRingHom g) / Polynomial.eval β (Polynomial.derivative (Polynomial.map (Polynomial.aeval t).toRingHom f)); Polynomial.eval t (Polynomial.map (Polynomial.aeval u).toRingHom (residueEliminant f g)) = 0

If β is a simple root of f(t, ·) and g has smaller z-degree than f, then the residue eliminant vanishes at t and u = g(t, β) / f'(t, β).