trans — Mathlib

English

Liouville property is transitive across towers of differential fields: if F ⊂ K ⊂ A with appropriate algebra structures, then IsLiouville(F,A) holds when IsLiouville(F,K) and IsLiouville(K,A).

Русский

Свойство Liouville транзитивно по цепочке полей: если F ⊂ K ⊂ A, то при условиях дифференциальной структуры IsLiouville(F,A).

LaTeX

$$$\\mathrm{IsLiouville}(F,K) \\to \\mathrm{IsLiouville}(K,A) \\to \\mathrm{IsLiouville}(F,A)$$$

Lean4

theorem trans {A : Type*} [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 where
  isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0) (u : ι → A) (v : A)
    (h :
      a =
        ∑ x, c x * logDeriv (u x) +
          v′) :=
    by
    obtain ⟨ι₀, _, c₀, hc₀, u₀, v₀, h₀⟩ :=
      inst2.isLiouville (a : K) ι ((↑) ∘ c)
        (fun _ ↦ by simp only [Function.comp_apply, ← coe_deriv, lift_map_eq_zero_iff, hc]) ((↑) ∘ u) v
        (by simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply])
    have hc (x : ι₀) := mem_range_of_deriv_eq_zero F (hc₀ x)
    choose c₀ hc using hc
    apply inst1.isLiouville a ι₀ c₀ _ u₀ v₀
    · rw [h₀]
      simp [hc]
    · intro
      apply_fun ((↑) : F → K)
      · simp only [coe_deriv, hc, algebraMap.coe_zero]
        apply hc₀
      · apply FaithfulSMul.algebraMap_injective

Похожие утверждения