Documentation

TauCeti.RingTheory.Polynomial.Distinguished

The polynomial (1 + X) ^ n - 1 #

The polynomial (1 + X) ^ n - 1 over a ring R is monic of degree n for n ≠ 0, with constant coefficient 0 and, for 0 < k, k-th coefficient the binomial coefficient n.choose k. Over a commutative ring, when n = p ^ m is a power of a prime p, every binomial coefficient (p ^ m).choose k with 0 < k < p ^ m is divisible by p, so the polynomial is distinguished at the ideal (p): monic with all non-leading coefficients in (p). Over the p-adic integers this is the shape of divisor for which Mathlib's Weierstrass division in ℤ_p⟦X⟧ is available.

This is the polynomial cutting out the finite levels of the power-series coordinate on the completed group algebra ℤ_p[[Γ]] of a procyclic pro-p group Γ: at a level Γ ⧸ U of order p ^ m, the class of the topological generator satisfies σ ^ (p ^ m) = 1, so (1 + X) ^ (p ^ m) - 1 vanishes at X = σ - 1.

Main results #

source
@[simp]
theorem TauCeti.Polynomial.natDegree_one_add_X_pow_sub_one {R : Type u_1} [Ring R] [Nontrivial R] (n : ℕ) :
((1 + Polynomial.X) ^ n - 1).natDegree = n

The polynomial (1 + X) ^ n - 1 has natDegree equal to n. For n ≠ 0 this is its degree; at n = 0 the polynomial is 0, whose natDegree is 0 by convention.

source
theorem TauCeti.Polynomial.monic_one_add_X_pow_sub_one {R : Type u_1} [Ring R] {n : ℕ} (hn : n ≠ 0) :
((1 + Polynomial.X) ^ n - 1).Monic

The polynomial (1 + X) ^ n - 1 is monic for n ≠ 0.

source
theorem TauCeti.Polynomial.isDistinguishedAt_one_add_X_pow_sub_one {R : Type u_1} [CommRing R] {p : ℕ} (hp : Nat.Prime p) (m : ℕ) :
((1 + Polynomial.X) ^ p ^ m - 1).IsDistinguishedAt (Ideal.span {↑p})

(1 + X) ^ (p ^ m) - 1 is a distinguished polynomial at (p), for a prime p: it is monic, its constant coefficient is 0, and its other non-leading coefficients are the binomial coefficients (p ^ m).choose k with 0 < k < p ^ m, which p divides.