Liouville's theorem

A proof of Liouville's theorem. Follows Rosenlicht, M. Integration in finite terms.

Liouville field extension

This file defines Liouville field extensions, which are differential field extensions which satisfy a slight generalization of Liouville's theorem. Note that this definition doesn't appear in the literature, and we introduce it as part of the formalization of Liouville's theorem.

Main declarations

• IsLiouville: A field extension being Liouville
• isLiouville_of_finiteDimensional: all finite dimensional field extensions (of a field with characteristic 0) are Liouville.

class IsLiouville (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Differential F] [Differential K] [Algebra F K] : Prop

We say that a differential field extension K / F is Liouville if, whenever an element a ∈ F can be written as a = v + ∑ cᵢ * logDeriv uᵢ for v, cᵢ, uᵢ ∈ K and cᵢ constant, it can also be written in that way with v, cᵢ, uᵢ ∈ F.

• isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ (x : ι), (c x)′ = 0) (u : ι → K) (v : K) (h : ↑a = ∑ x : ι, ↑(c x) * Differential.logDeriv (u x) + v′) : ∃ (ι₀ : Type) (x : Fintype ι₀) (c₀ : ι₀ → F) (_ : ∀ (x : ι₀), (c₀ x)′ = 0) (u₀ : ι₀ → F) (v₀ : F), a = ∑ x : ι₀, c₀ x * Differential.logDeriv (u₀ x) + v₀′

instance IsLiouville.rfl (F : Type u_1) [Field F] [Differential F] : IsLiouville F F

theorem IsLiouville.trans (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Differential F] [Differential K] [Algebra F K] [DifferentialAlgebra F K] {A : Type u_3} [Field A] [Algebra K A] [Algebra F A] [Differential A] [IsScalarTower F K A] [Differential.ContainConstants F K] (inst1 : IsLiouville F K) (inst2 : IsLiouville K A) : IsLiouville F A

instance instIsLiouvilleSubtypeMemIntermediateField {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Differential F] [Differential K] [Algebra F K] [DifferentialAlgebra F K] [CharZero F] (B : IntermediateField F K) [FiniteDimensional F ↥B] [inst : IsLiouville F K] : IsLiouville F ↥B

If K is a Liouville extension of F and B is a finite dimensional intermediate field K / B / F, then it's also a Liouville extension of F.

theorem IsLiouville.equiv {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Differential F] [Differential K] [Algebra F K] [DifferentialAlgebra F K] [CharZero F] {K' : Type u_3} [Field K'] [Differential K'] [Algebra F K'] [DifferentialAlgebra F K'] [Algebra.IsAlgebraic F K'] [inst : IsLiouville F K] (e : K ≃ₐ[F] K') : IsLiouville F K'

Transfer an IsLiouville instance using an equivalence K ≃ₐ[F] K'. Requires an algebraic K' to show that the equivalence commutes with the derivative.

instance isLiouville_of_finiteDimensional {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Differential F] [Differential K] [Algebra F K] [DifferentialAlgebra F K] [CharZero F] [FiniteDimensional F K] : IsLiouville F K

We lift isLiouville_of_finiteDimensional_galois to non-Galois field extensions by using it for the normal closure then obtaining it for F.