Cartier operators on power series

The Cartier operator of modulus q and index r selects coefficients at the indices q * n + r. It is linear in the series. For an actual residue r < q, it commutes with multiplication by an expanded series, and the expanded Cartier components reconstruct the original series. Over a finite field, expansion by its cardinality is the Frobenius power, so these identities give the usual Cartier identities used in residue averaging. Since the j-th iterate of that expansion is the q ^ j-th power map (FiniteField.PowerSeries.expand_card_pow_apply), for a set T of series stable under the Cartier operators of modulus q = |K|, the powers h ^ q ^ j with h ∈ T lie in the K[X]-span of the powers g ^ q ^ m with g ∈ T whenever j ≤ m; this is the linear-algebra step of the proof of Christol's theorem. A series whose coefficients vanish away from the multiples of the modulus is the expansion of its residue-zero Cartier component; in prime characteristic this applies to a series with zero derivative.

The definition and finite-field multiplication identity follow Section 3, definition and Proposition 4, of Rowland–Stipulanti–Yassawi, An elementary proof of Bridy's theorem (https://arxiv.org/html/2308.10977v2). The substitution identities use Mathlib's PowerSeries.expand; the finite-field specializations use FiniteField.PowerSeries.expand_card.

noncomputable def PowerSeries.cartier (R : Type u_1) [Semiring R] (q r : ℕ) : PowerSeries R →ₗ[R] PowerSeries R

The Cartier operator selects the coefficients at q * n + r. It is defined for every index r; the multiplication identities require r < q.

@[simp]

theorem PowerSeries.coeff_cartier {R : Type u_1} [Semiring R] (q r n : ℕ) (F : PowerSeries R) : (coeff n) ((cartier R q r) F) = (coeff (q * n + r)) F

The defining coefficient equation of a Cartier operator.

@[simp]

theorem PowerSeries.constantCoeff_cartier {R : Type u_1} [Semiring R] (q r : ℕ) (F : PowerSeries R) : constantCoeff ((cartier R q r) F) = (coeff r) F

The constant coefficient of a Cartier component is the coefficient at its index.

@[simp]

theorem PowerSeries.cartier_one_zero {R : Type u_1} [Semiring R] : cartier R 1 0 = LinearMap.id

The residue-zero Cartier operator of modulus one is the identity.

@[simp]

theorem PowerSeries.cartier_one {R : Type u_1} [Semiring R] (q r : ℕ) (hq : q ≠ 0) : (cartier R q r) 1 = if r = 0 then 1 else 0

At nonzero modulus, the Cartier components of 1 vanish except at residue zero. This holds even when r lies outside the residue range.

@[simp]

theorem PowerSeries.cartier_monomial {R : Type u_1} [Semiring R] (q r m : ℕ) (hr : r < q) (a : R) : (cartier R q r) ((monomial m) a) = if m % q = r then (monomial (m / q)) a else 0

On a monomial, a Cartier operator keeps precisely its residue class.

theorem PowerSeries.exists_cartier_coe_polynomial_eq {R : Type u_1} [Semiring R] (q r : ℕ) (hq : q ≠ 0) (P : Polynomial R) : ∃ (P' : Polynomial R), P'.natDegree ≤ P.natDegree / q ∧ (cartier R q r) ↑P = ↑P'

At nonzero modulus, a Cartier operator sends a polynomial to a polynomial whose degree is at most the original degree divided by the modulus. This holds for every index r.

theorem PowerSeries.cartier_expand_mul {R : Type u_1} [CommRing R] (q r : ℕ) (hq : q ≠ 0) (hr : r < q) (F G : PowerSeries R) : (cartier R q r) ((expand q hq) F * G) = F * (cartier R q r) G

Multiplication by an expanded series passes through a Cartier operator at an actual residue.

theorem PowerSeries.sum_X_pow_mul_expand_cartier {R : Type u_1} [CommRing R] (q : ℕ) (hq : q ≠ 0) (F : PowerSeries R) : F = ∑ r ∈ Finset.range q, X ^ r * (expand q hq) ((cartier R q r) F)

Every series is the sum of its expanded Cartier components, one for each residue.

theorem PowerSeries.expand_cartier_zero_of_coeff_eq_zero {R : Type u_1} [CommRing R] (q : ℕ) (hq : q ≠ 0) {F : PowerSeries R} (hF : ∀ (n : ℕ), ¬q ∣ n → (coeff n) F = 0) : (expand q hq) ((cartier R q 0) F) = F

A series whose coefficients vanish away from the multiples of q is the expansion of its residue-zero Cartier component.

theorem PowerSeries.expand_cartier_of_derivative_eq_zero {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {f : PowerSeries R} (hf : derivative f = 0) : (expand p ⋯) ((cartier R p 0) f) = f

The residue-zero Cartier component recovers a series with zero derivative by expansion in prime characteristic.

theorem PowerSeries.cartier_pow_card_mul {K : Type u_1} [Field K] [Fintype K] (r : ℕ) (hr : r < Fintype.card K) (F G : PowerSeries K) : (cartier K (Fintype.card K) r) (F ^ Fintype.card K * G) = F * (cartier K (Fintype.card K) r) G

Over a finite field, multiplication by a cardinality power passes through a Cartier operator at an actual residue.

theorem PowerSeries.eq_sum_X_pow_mul_cartier_pow {K : Type u_1} [Field K] [Fintype K] (F : PowerSeries K) : F = ∑ r ∈ Finset.range (Fintype.card K), X ^ r * (cartier K (Fintype.card K) r) F ^ Fintype.card K

Over a finite field, a series is the sum of the cardinality powers of its Cartier components multiplied by the corresponding powers of X.

theorem PowerSeries.pow_card_pow_mem_span_of_cartier_stable {K : Type u_1} [Field K] [Fintype K] {T : Set (PowerSeries K)} (hTq : ∀ h ∈ T, ∀ r < Fintype.card K, (cartier K (Fintype.card K) r) h ∈ T) {h : PowerSeries K} (hh : h ∈ T) {j m : ℕ} (hjm : j ≤ m) : h ^ Fintype.card K ^ j ∈ Submodule.span (Polynomial K) ((fun (x : PowerSeries K) => x ^ Fintype.card K ^ m) '' T)

Over a finite field K with q elements, let T be a set of power series that is stable under the Cartier operators cartier K q r with r < q. For h ∈ T and j ≤ m, the power h ^ q ^ j lies in the K[X]-span of the powers g ^ q ^ m with g ∈ T.

The small examples also check the residue restriction in the multiplication identities.