mathlib docs: ring_theory.witt

The Frobenius operator #

If R has characteristic p, then there is a ring endomorphism frobenius R p that raises r : R to the power p. By applying witt_vector.map to frobenius R p, we obtain a ring endomorphism 𝕎 R →+* 𝕎 R. It turns out that this endomorphism can be described by polynomials over ℤ that do not depend on R or the fact that it has characteristic p. In this way, we obtain a Frobenius endomorphism witt_vector.frobenius_fun : 𝕎 R → 𝕎 R for every commutative ring R.

Unfortunately, the aforementioned polynomials can not be obtained using the machinery of witt_structure_int that was developed in structure_polynomial.lean. We therefore have to define the polynomials by hand, and check that they have the required property.

In case R has characteristic p, we show in frobenius_fun_eq_map_frobenius that witt_vector.frobenius_fun is equal to witt_vector.map (frobenius R p).

Main definitions and results #

frobenius_poly: the polynomials that describe the coefficients of frobenius_fun;
frobenius_fun: the Frobenius endomorphism on Witt vectors;
frobenius_fun_is_poly: the tautological assertion that Frobenius is a polynomial function;
frobenius_fun_eq_map_frobenius: the fact that in characteristic p, Frobenius is equal to witt_vector.map (frobenius R p).

TODO: Show that witt_vector.frobenius_fun is a ring homomorphism, and bundle it into witt_vector.frobenius.

References #

source

def witt_vector.frobenius_poly_rat (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

mv_polynomial ℕ ℚ

The rational polynomials that give the coefficients of frobenius x, in terms of the coefficients of x. These polynomials actually have integral coefficients, see frobenius_poly and map_frobenius_poly.

Equations

witt_vector.frobenius_poly_rat p n = ⇑(mv_polynomial.bind₁ (witt_polynomial p ℚ ∘ λ (n : ℕ), n + 1)) (X_in_terms_of_W p ℚ n)

source

theorem witt_vector.bind₁_frobenius_poly_rat_witt_polynomial (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

⇑(mv_polynomial.bind₁ (witt_vector.frobenius_poly_rat p)) (witt_polynomial p ℚ n) = witt_polynomial p ℚ (n + 1)

source

def witt_vector.frobenius_poly_aux (p : ℕ) [hp : fact (nat.prime p)] :

ℕ → mv_polynomial ℕ ℤ

An auxilliary polynomial over the integers, that satisfies (frobenius_poly_aux p n - X n ^ p) / p = frobenius_poly p n. This makes it easy to show that frobenius_poly p n is congruent to X n ^ p modulo p.

Equations

witt_vector.frobenius_poly_aux p n = mv_polynomial.X (n + 1) - ∑ (i : fin n), ∑ (j : ℕ) in finset.range (p ^ (n - ↑i)), (((mv_polynomial.X ↑i ^ p) ^ (p ^ (n - ↑i) - (j + 1))) * witt_vector.frobenius_poly_aux p ↑i ^ (j + 1)) * ⇑mv_polynomial.C (↑((p ^ (n - ↑i)).choose (j + 1) / p ^ (n - ↑i - pnat_multiplicity p ⟨j + 1, _⟩)) * ↑p ^ (j - pnat_multiplicity p ⟨j + 1, _⟩))

source

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

witt_vector.frobenius_poly_aux p n = mv_polynomial.X (n + 1) - ∑ (i : ℕ) in finset.range n, ∑ (j : ℕ) in finset.range (p ^ (n - i)), (((mv_polynomial.X i ^ p) ^ (p ^ (n - i) - (j + 1))) * witt_vector.frobenius_poly_aux p i ^ (j + 1)) * ⇑mv_polynomial.C (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - pnat_multiplicity p ⟨j + 1, _⟩)) * ↑p ^ (j - pnat_multiplicity p ⟨j + 1, _⟩))

source

def witt_vector.frobenius_poly (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

mv_polynomial ℕ ℤ

The polynomials that give the coefficients of frobenius x, in terms of the coefficients of x.

Equations

witt_vector.frobenius_poly p n = mv_polynomial.X n ^ p + (⇑mv_polynomial.C ↑p) * witt_vector.frobenius_poly_aux p n

source

theorem witt_vector.map_frobenius_poly.key₁ (p : ℕ) [hp : fact (nat.prime p)] (n j : ℕ) (hj : j < p ^ n) :

p ^ (n - pnat_multiplicity p ⟨j + 1, _⟩) ∣ (p ^ n).choose (j + 1)

A key divisibility fact for the proof of witt_vector.map_frobenius_poly.

source

theorem witt_vector.map_frobenius_poly.key₂ (p : ℕ) [hp : fact (nat.prime p)] {n i j : ℕ} (hi : i < n) (hj : j < p ^ (n - i)) :

j - pnat_multiplicity p ⟨j + 1, _⟩ + n = i + j + (n - i - pnat_multiplicity p ⟨j + 1, _⟩)

A key numerical identity needed for the proof of witt_vector.map_frobenius_poly.

source

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

⇑(mv_polynomial.map (int.cast_ring_hom ℚ)) (witt_vector.frobenius_poly p n) = witt_vector.frobenius_poly_rat p n

source

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

⇑(mv_polynomial.map (int.cast_ring_hom (zmod p))) (witt_vector.frobenius_poly p n) = mv_polynomial.X n ^ p

source

@[simp]

theorem witt_vector.bind₁_frobenius_poly_witt_polynomial (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

⇑(mv_polynomial.bind₁ (witt_vector.frobenius_poly p)) (witt_polynomial p ℤ n) = witt_polynomial p ℤ (n + 1)

source

def witt_vector.frobenius_fun {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) :

witt_vector p R

frobenius_fun is the function underlying the ring endomorphism frobenius : 𝕎 R →+* frobenius 𝕎 R.

Equations

x.frobenius_fun = witt_vector.mk p (λ (n : ℕ), ⇑(mv_polynomial.aeval x.coeff) (witt_vector.frobenius_poly p n))

source

theorem witt_vector.coeff_frobenius_fun {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : ℕ) :

x.frobenius_fun.coeff n = ⇑(mv_polynomial.aeval x.coeff) (witt_vector.frobenius_poly p n)

source

theorem witt_vector.frobenius_fun_is_poly (p : ℕ) [hp : fact (nat.prime p)] :

witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.frobenius_fun)

frobenius_fun is tautologically a polynomial function.