Coordinates of a derivation in a finite field-extension basis

Proved

OAI.PiExponent.derivation_basis_coordinates

by marwahaha · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebranumber-theoryopenai-pi-exponent-017

Let $k\subseteq F\subseteq E$ be a compatible field tower with compatible $k$ -derivations $d$ on $F$ and $D$ on $E$ . For a finite $F$ -basis $(b_j)$ of $E$ , an element $z=\sum_j z_jb_j$ , and every index $i$ ,

[D(z)]_i=d(z_i)+\sum_j z_j[D(b_j)]_i.

The formula records both differentiation of the coordinates and variation of the basis.

Preamble

import Mathlib.Algebra.Polynomial.Derivation
import Mathlib.Algebra.Polynomial.Div
import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.Trace.Defs
import Mathlib.Tactic


namespace OAI
namespace PiExponent
end PiExponent
end OAI
open scoped LaurentSeries Matrix
open Polynomial
open OAI.PiExponent

Formal statement

theorem OAI.PiExponent.derivation_basis_coordinates
    {k F E ι : Type*} [Field k] [Field F] [Field E] [Fintype ι]
    [Algebra k F] [Algebra k E] [Algebra F E] [IsScalarTower k F E]
    (d : Derivation k F F) (D : Derivation k E E)
    (hcompat : ∀ a : F, D (algebraMap F E a) = algebraMap F E (d a))
    (b : Module.Basis ι F E) (z : E) (i : ι) :
    b.repr (D z) i = d (b.repr z i) +
      ∑ j, b.repr z j * b.repr (D (b j)) i := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LogarithmicObstruction.lean#L111-L124

View graph