Iterating X d/dX over ZMod p

Over ZMod p, the operator D = X · d/dX acts on X^m as multiplication by m. Iterating it p − 1 times kills exactly the monomials whose exponent is divisible by p and fixes the others (Fermat's little theorem): D^[p−1] is the identity minus the projection onto the p-divisible exponents, the kernel of the Cartier operator.

Main results

• ConjeturaC.D_iter_X_pow: D^[k] (X^m) = C (m^k) * X^m.
• ConjeturaC.D_iter_card_sub_one: D^[p−1] (X^m) = if p ∣ m then 0 else X^m.
• ConjeturaC.D_iter_cartier: D^[p−1] f = f − ∑_{m ∈ supp f, p ∣ m} C (f.coeff m) * X^m.

noncomputable def ConjeturaC.D (p : ℕ) (f : Polynomial (ZMod p)) : Polynomial (ZMod p)

The Euler operator D f = X * f' on (ZMod p)[X].

Equations

• ConjeturaC.D p f = Polynomial.X * Polynomial.derivative f

noncomputable def ConjeturaC.Dlin (p : ℕ) : Module.End (ZMod p) (Polynomial (ZMod p))

D as a linear endomorphism.

Equations

• ConjeturaC.Dlin p = LinearMap.mulLeft (ZMod p) Polynomial.X ∘ₗ Polynomial.derivative

theorem ConjeturaC.D_iter_eq {p : ℕ} (k : ℕ) : (D p)^[k] = ⇑(Dlin p ^ k)

theorem ConjeturaC.D_C_mul_X_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ZMod p) (m : ℕ) : D p (Polynomial.C a * Polynomial.X ^ m) = Polynomial.C (a * ↑m) * Polynomial.X ^ m

theorem ConjeturaC.D_iter_C_mul_X_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ZMod p) (k m : ℕ) : (D p)^[k] (Polynomial.C a * Polynomial.X ^ m) = Polynomial.C (a * ↑m ^ k) * Polynomial.X ^ m

theorem ConjeturaC.D_iter_X_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (k m : ℕ) : (D p)^[k] (Polynomial.X ^ m) = Polynomial.C (↑m ^ k) * Polynomial.X ^ m

(a)

theorem ConjeturaC.pow_card_sub_one_natCast {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : ↑m ^ (p - 1) = if p ∣ m then 0 else 1

theorem ConjeturaC.D_iter_card_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : (D p)^[p - 1] (Polynomial.X ^ m) = if p ∣ m then 0 else Polynomial.X ^ m

(b)

theorem ConjeturaC.D_iter_cartier {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) : (D p)^[p - 1] f = f - ∑ m ∈ f.support with p ∣ m, Polynomial.C (f.coeff m) * Polynomial.X ^ m

(c)