Liouville's theorem for algebraic extensions

Stream: maths

[Daniel Weber]

I'm trying to prove Liouville's theorem (in differential algebra), and currently I'm working on the algebraic case, that is:

If $a \in F, a = \sum c_i \frac{u_i'}{u_i} + v'$ for $c_i \in F, u_i \in F(\alpha), v \in F(\alpha)$ where $\alpha$ is algebraic over $F$, then there exists $d_i, w_i, x \in F$ such that $\alpha = \sum d_i \frac{w_i'}{w_i} + x'$.

The proof of this goes like this:
We can write $u_i, v$ as $u_i(\alpha), v(\alpha)$ for $u_i, v \in F[x]$.
We want to show that $a = \sum c_i \frac{u_i(\beta)'}{u_i(\beta)} + v(\beta)'$ for all conjugates of $\alpha$, then we average all of those, and we get $a = \sum \frac{c_i}s \frac{(u_i(\beta_1) u_i(\beta_2) \cdots u_i(\beta_s))'}{u_i(\beta_1) u_i(\beta_2) \cdots u_i(\beta_s)} + (\frac{v(\beta_1) + v(\beta_2) + \cdots + v(\beta_s)}s)'$.
All of these expressions are symmetric polynomials in the conjugates of $\alpha$, so by Vieta's formulas and the fundamental theorem of symmetric polynomials those are actually in $F$.

To show that $a = \sum c_i \frac{u_i(\beta)'}{u_i(\beta)} + v(\beta)'$ we show that $\beta' = h(\beta)$ where $h$ is a polynomial defined by the minimal polynomial of $\beta$, so we can expand all of this to an evaluation of a rational function at $\beta$, and if the result is $a \in F$ for $\alpha$ then that's also the case for its conjugates.

I think I can formalize the statement:

variable {F K : Type*} [DifferentialField F] [DecidableEq F] [CharZero F] [DifferentialField K] [DifferentialAlgebra F K]

open IntermediateField

theorem liouville_algebraic (a : F) (ι : Type*) [Fintype ι] (c : ι → F) (hc : ∀ x, IsConstant (c x))
    (g : K) (hg : IsAlgebraic F g) (u : ι → F⟮g⟯) (v : F⟮g⟯) (h : a = ∑ x, c x * (u x)′ / (u x) + v′) :
    ∃ (c' : ι → F) (u' : ι → F) (v' : F), (∀ x, IsConstant (c' x)) ∧ (a = ∑ x, c' x * (u' x)′ / (u' x) + v'′) := by
  sorry

However, I'm very uncertain about the proof. I think I want to extend docs#AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly to a differential equivalence, and apply it to h.
Then I want to lift all of these equations to the splitting field of minpoly F g and add them up, but I'm not sure how to do that. And then somehow convert it to a MvPolynomial, to apply the fundamental theorem of symmetric polynomials?

Any suggestions for a reasonable way to do all of this?

[Daniel Weber]

Perhaps this might be easier to do with Galois theory instead of the fundamental theorem of symmetric polynomials, but I'm not sure how to do that either

[Daniel Weber]

I managed to come up with the following proof plan. Does it seem workable?

First, we start by proving the result for finite dimensional Galois extensions.
To do this, first we show that automorphims which fix the base field commute with the derivative, over algebraic extensions.
Then we average the equation $a = \sum c_i \frac{u_i'}{u_i} + v'$ over all automorphisms which fix $F$.
After reordering the terms on the RHS, we show that each relevant term is fixed by all those automorphisms, and because the extension is Galois we get that the elements are in $F$.
This avoids the need to work with polynomials too much.

For F⟮g⟯, I think it's possible just lift everything to the splitting field of minpoly F g, but I'm not sure how to do that in practice.

[Johan Commelin]

I think going for the fin.dim case first is indeed a good idea

[Adam Topaz]

I think your strategy to first prove it in the finite Galois case is the right way to go! And in the general case, I wouldn't do it directly for fields of the form F(g), but rather just some finite extension M|F, which you can embed in some Galois closure over F. In the general case of a non-finite algebraic extension M|F, since you're dealing with a finite sum, the equation is contained in some finite subextension, so you can reduce it more easily to that if you don't assume it has the form F(g) directly. (Of course, since this is characteristic 0, all finite extensions are primitive, but assuming it's primitive doesn't seem to make your life any easier!)

[Daniel Weber]

Thanks. For the Galois closure I can just use docs#normalClosure, right?