mathlib3 documentation

ring_theory.witt_vector.witt_polynomial

Witt polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

To endow witt_vector p R with a ring structure, we need to study the so-called Witt polynomials.

Fix a base value p : ℕ. The p-adic Witt polynomials are an infinite family of polynomials indexed by a natural number n, taking values in an arbitrary ring R. The variables of these polynomials are represented by natural numbers. The variable set of the nth Witt polynomial contains at most n+1 elements {0, ..., n}, with exactly these variables when R has characteristic 0.

These polynomials are used to define the addition and multiplication operators on the type of Witt vectors. (While this type itself is not complicated, the ring operations are what make it interesting.)

When the base p is invertible in R, the p-adic Witt polynomials form a basis for mv_polynomial ℕ R, equivalent to the standard basis.

Main declarations #

witt_polynomial p R n: the n-th Witt polynomial, viewed as polynomial over the ring R
X_in_terms_of_W p R n: if p is invertible, the polynomial X n is contained in the subalgebra generated by the Witt polynomials. X_in_terms_of_W p R n is the explicit polynomial, which upon being bound to the Witt polynomials yields X n.
bind₁_witt_polynomial_X_in_terms_of_W: the proof of the claim that bind₁ (X_in_terms_of_W p R) (W_ R n) = X n
bind₁_X_in_terms_of_W_witt_polynomial: the converse of the above statement

Notation #

In this file we use the following notation

p is a natural number, typically assumed to be prime.
R and S are commutative rings
W n (and W_ R n when the ring needs to be explicit) denotes the nth Witt polynomial

References #

noncomputable def witt_polynomial (p : ℕ) (R : Type u_1) [comm_ring R] (n : ℕ) :

mv_polynomial ℕ R

witt_polynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Equations

witt_polynomial p R n = (finset.range (n + 1)).sum (λ (i : ℕ), ⇑(mv_polynomial.monomial (finsupp.single i (p ^ (n - i)))) (↑p ^ i))

theorem witt_polynomial_eq_sum_C_mul_X_pow (p : ℕ) (R : Type u_1) [comm_ring R] (n : ℕ) :

witt_polynomial p R n = (finset.range (n + 1)).sum (λ (i : ℕ), ⇑mv_polynomial.C (↑p ^ i) * mv_polynomial.X i ^ p ^ (n - i))

We set up notation locally to this file, to keep statements short and comprehensible. This allows us to simply write W n or W_ ℤ n.

@[simp]

theorem map_witt_polynomial (p : ℕ) {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (f : R →+* S) (n : ℕ) :

⇑(mv_polynomial.map f) (witt_polynomial p R n) = witt_polynomial p S n

@[simp]

theorem constant_coeff_witt_polynomial (p : ℕ) (R : Type u_1) [comm_ring R] [hp : fact (nat.prime p)] (n : ℕ) :

⇑mv_polynomial.constant_coeff (witt_polynomial p R n) = 0

@[simp]

theorem witt_polynomial_zero (p : ℕ) (R : Type u_1) [comm_ring R] :

witt_polynomial p R 0 = mv_polynomial.X 0

@[simp]

theorem witt_polynomial_one (p : ℕ) (R : Type u_1) [comm_ring R] :

witt_polynomial p R 1 = ⇑mv_polynomial.C ↑p * mv_polynomial.X 1 + mv_polynomial.X 0 ^ p

theorem aeval_witt_polynomial (p : ℕ) (R : Type u_1) [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] (f : ℕ → A) (n : ℕ) :

⇑(mv_polynomial.aeval f) (witt_polynomial p R n) = (finset.range (n + 1)).sum (λ (i : ℕ), ↑p ^ i * f i ^ p ^ (n - i))

@[simp]

theorem witt_polynomial_zmod_self (p n : ℕ) :

witt_polynomial p (zmod (p ^ (n + 1))) (n + 1) = ⇑(mv_polynomial.expand p) (witt_polynomial p (zmod (p ^ (n + 1))) n)

Over the ring zmod (p^(n+1)), we produce the n+1st Witt polynomial by expanding the nth Witt polynomial by p.

theorem witt_polynomial_vars (p : ℕ) (R : Type u_1) [comm_ring R] [hp : ne_zero p] [char_zero R] (n : ℕ) :

(witt_polynomial p R n).vars = finset.range (n + 1)

theorem witt_polynomial_vars_subset (p : ℕ) (R : Type u_1) [comm_ring R] [hp : ne_zero p] (n : ℕ) :

(witt_polynomial p R n).vars ⊆ finset.range (n + 1)

Witt polynomials as a basis of the polynomial algebra #

If p is invertible in R, then the Witt polynomials form a basis of the polynomial algebra mv_polynomial ℕ R. The polynomials X_in_terms_of_W give the coordinate transformation in the backwards direction.

noncomputable def X_in_terms_of_W (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] :

ℕ → mv_polynomial ℕ R

The X_in_terms_of_W p R n is the polynomial on the basis of Witt polynomials that corresponds to the ordinary X n.

Equations

X_in_terms_of_W p R n = (mv_polynomial.X n - finset.univ.sum (λ (i : fin n), ⇑mv_polynomial.C (↑p ^ ↑i) * X_in_terms_of_W p R ↑i ^ p ^ (n - ↑i))) * ⇑mv_polynomial.C (⅟ ↑p ^ n)

theorem X_in_terms_of_W_eq (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] {n : ℕ} :

X_in_terms_of_W p R n = (mv_polynomial.X n - (finset.range n).sum (λ (i : ℕ), ⇑mv_polynomial.C (↑p ^ i) * X_in_terms_of_W p R i ^ p ^ (n - i))) * ⇑mv_polynomial.C (⅟ ↑p ^ n)

@[simp]

theorem constant_coeff_X_in_terms_of_W (p : ℕ) (R : Type u_1) [comm_ring R] [hp : fact (nat.prime p)] [invertible ↑p] (n : ℕ) :

⇑mv_polynomial.constant_coeff (X_in_terms_of_W p R n) = 0

@[simp]

theorem X_in_terms_of_W_zero (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] :

X_in_terms_of_W p R 0 = mv_polynomial.X 0

theorem X_in_terms_of_W_vars_aux (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

n ∈ (X_in_terms_of_W p ℚ n).vars ∧ (X_in_terms_of_W p ℚ n).vars ⊆ finset.range (n + 1)

theorem X_in_terms_of_W_vars_subset (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(X_in_terms_of_W p ℚ n).vars ⊆ finset.range (n + 1)

theorem X_in_terms_of_W_aux (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] (n : ℕ) :

X_in_terms_of_W p R n * ⇑mv_polynomial.C (↑p ^ n) = mv_polynomial.X n - (finset.range n).sum (λ (i : ℕ), ⇑mv_polynomial.C (↑p ^ i) * X_in_terms_of_W p R i ^ p ^ (n - i))

@[simp]

theorem bind₁_X_in_terms_of_W_witt_polynomial (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] (k : ℕ) :

⇑(mv_polynomial.bind₁ (X_in_terms_of_W p R)) (witt_polynomial p R k) = mv_polynomial.X k

@[simp]

theorem bind₁_witt_polynomial_X_in_terms_of_W (p : ℕ) (R : Type u_1) [comm_ring R] [invertible ↑p] (n : ℕ) :

⇑(mv_polynomial.bind₁ (witt_polynomial p R)) (X_in_terms_of_W p R n) = mv_polynomial.X n