Residues of closed rational one-forms at simple polynomial roots. The polynomial proof avoids needing a partial-fraction decomposition.
theorem
CCDN.derivative_differential_mapCoeffs
{K : Type u_1}
[Field K]
[Differential K]
(f : Polynomial K)
:
Coefficientwise differentiation commutes with the formal derivative of polynomials.
theorem
CCDN.closed_form_residue_deriv_eq_zero
{K : Type u_1}
[Field K]
[Differential K]
(f p q : Polynomial K)
(c : K)
(hroot : (Polynomial.aeval c) f = 0)
(hsimple : (Polynomial.aeval c) (Polynomial.derivative f) ≠ 0)
(hclosed :
Differential.mapCoeffs p * f - p * Differential.mapCoeffs f = Polynomial.derivative q * f - q * Polynomial.derivative f)
:
A closed rational one-form has differentially constant residue at every simple root of its denominator. The equation is written after clearing f².
theorem
CCDN.differential_mapCoeffs_map
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Differential K]
[Differential L]
[Algebra K L]
[DifferentialAlgebra K L]
(p : Polynomial K)
:
Differential.mapCoeffs (Polynomial.map (algebraMap K L) p) = Polynomial.map (algebraMap K L) (Differential.mapCoeffs p)
Coefficientwise differentiation commutes with extending coefficients along a differential
algebra K → L.
theorem
CCDN.closed_form_eq_constant_gradient_of_residue_mem_base
{F : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Field F]
[Field K]
[Field L]
[Algebra F K]
[Algebra K L]
[Algebra F L]
[IsScalarTower F K L]
[Differential K]
(f p q : Polynomial K)
(hf : Irreducible f)
(hm : f.Monic)
(c : L)
(hc : (Polynomial.aeval c) f = 0)
(hsimple : (Polynomial.aeval c) (Polynomial.derivative f) ≠ 0)
(hpdeg : p.degree < f.degree)
(hqdeg : q.degree < f.degree)
(hclosed :
Differential.mapCoeffs p * f - p * Differential.mapCoeffs f = Polynomial.derivative q * f - q * Polynomial.derivative f)
(hres : (Polynomial.aeval c) p / (Polynomial.aeval c) (Polynomial.derivative f) ∈ (algebraMap F L).range)
:
∃ (a : F),
p = Polynomial.C ((algebraMap F K) a) * Polynomial.derivative f ∧ q = Polynomial.C ((algebraMap F K) a) * Differential.mapCoeffs f
For a monic irreducible denominator, a closed form with a single base-field residue is a constant multiple of its logarithmic differential. Only the displayed residue must descend, not every differential constant in the root field.