Christol's theorem

TheoremChristol's theorem#✓fully proved

Let \(p\) be a prime, \(r \ge 1\) a natural number, and \(K\) a finite field of characteristic \(p\) with \(q = p^r\) elements. A formal power series \(f = \sum_n f_n X^n \in K[[X]]\) is algebraic over the polynomial ring \(K[X]\) (it is a root of a nonzero polynomial with coefficients in \(K[X]\)) if and only if its coefficient sequence \(n \mapsto f_n\) is \(p\)-automatic, that is, its \(p\)-kernel is finite.

Algebraicity over \(K[X]\) is the denominator-cleared form of algebraicity over the rational function field \(K(X)\); it is not integrality over \(K[X]\). Automaticity is taken in base \(p\), not in base \(q\).

public theorem christol_theorem (K : Type*) [Field K] [Finite K] (p q r : ℕ)
    [CharP K p] (hp : Nat.Prime p) (hcard : Nat.card K = q) (hq : q = p ^ r)
    (hr : 0 < r) (f : PowerSeries K) :
    IsAlgebraic (Polynomial K) f ↔ IsKAutomatic p (fun n => PowerSeries.coeff n f)

Sources

• Adamczewski--Bell, arXiv:1205.4091v1, lines 260--265: for q a positive integral power of the characteristic prime p, a series over F_q is algebraic over F_q(t) iff its coefficient sequence is p-automatic.

Uses 6 · Used by 1

Statement uses\(k\)-automatic sequence (finite-kernel definition)

Proof usesThe \(q\)-kernel is closed under decimation · Finiteness of the \(p\)-kernel from the \(p^r\)-kernel · The \(p^r\)-kernel lies in the \(p\)-kernel · A sequence lies in its own kernel · The \(k\)-kernel of a sequence

Used byChristol's theorem, automaton form

TheoremChristol's theorem, automaton form#✓fully proved

Let \(p\) be a prime, \(r \ge 1\) a natural number, and \(K\) a finite field of characteristic \(p\) with \(q = p^r\) elements. A formal power series \(f = \sum_n f_n X^n \in K[[X]]\) is algebraic over the polynomial ring \(K[X]\) (it is a root of a nonzero polynomial with coefficients in \(K[X]\)) if and only if its coefficient sequence \(n \mapsto f_n\) is \(p\)-automatic in the sense of finite automata with output.

public theorem christol_theorem_isKAutomaticSequence (K : Type) [Field K] [Fintype K]
    (p q r : ℕ) [CharP K p] (hp : Nat.Prime p) (hcard : Nat.card K = q)
    (hq : q = p ^ r) (hr : 0 < r) (f : PowerSeries K) :
    IsAlgebraic (Polynomial K) f
      ↔ IsKAutomaticSequence p (fun n => PowerSeries.coeff n f)

Uses 4

Statement usesAutomatic sequences via finite automata

Proof uses\(k\)-automatic sequence (finite-kernel definition) · Christol's theorem · Eilenberg's theorem: finite kernel iff automatic

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.