# mathlibdocumentation

ring_theory.witt_vector.frobenius

## 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 #

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

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
noncomputable def witt_vector.frobenius_poly_aux (p : ) [hp : fact (nat.prime p)] :

An auxiliary polynomial over the integers, that satisfies p * (frobenius_poly_aux p n) + X n ^ 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
theorem witt_vector.frobenius_poly_aux_eq (p : ) [hp : fact (nat.prime p)] (n : ) :
= mv_polynomial.X (n + 1) - (finset.range n).sum (λ (i : ), (finset.range (p ^ (n - i))).sum (λ (j : ), ^ p) ^ (p ^ (n - i) - (j + 1)) * ^ (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, _⟩))))
noncomputable def witt_vector.frobenius_poly (p : ) [hp : fact (nat.prime p)] (n : ) :

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

Equations
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.

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.

theorem witt_vector.map_frobenius_poly (p : ) [hp : fact (nat.prime p)] (n : ) :
theorem witt_vector.frobenius_poly_zmod (p : ) [hp : fact (nat.prime p)] (n : ) :
=
@[simp]
theorem witt_vector.bind₁_frobenius_poly_witt_polynomial (p : ) [hp : fact (nat.prime p)] (n : ) :
= (n + 1)
noncomputable def witt_vector.frobenius_fun {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) :
R

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

Equations
Instances for witt_vector.frobenius_fun
theorem witt_vector.coeff_frobenius_fun {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (n : ) :
theorem witt_vector.frobenius_fun_is_poly (p : ) [hp : fact (nat.prime p)] :
(λ (R : Type u_1) (_Rcr : , witt_vector.frobenius_fun)

frobenius_fun is tautologically a polynomial function.

See also frobenius_is_poly.

@[instance]
def witt_vector.frobenius_fun_is_poly.comp_i (p : ) [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : , (λ (R : Type u_1) (_Rcr : , witt_vector.frobenius_fun) R _Rcr f)
@[instance]
def witt_vector.frobenius_fun_is_poly.comp₂_i (p : ) [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : (x y : R), (λ (R : Type u_1) (_Rcr : , witt_vector.frobenius_fun) R _Rcr (f x y))
theorem witt_vector.ghost_component_frobenius_fun {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ) (x : R) :
noncomputable def witt_vector.frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
R →+* R

If R has characteristic p, then there is a ring endomorphism that raises r : R to the power p. By applying witt_vector.map to this endomorphism, we obtain a ring endomorphism frobenius R p : 𝕎 R →+* 𝕎 R.

The underlying function of this morphism is witt_vector.frobenius_fun.

Equations
theorem witt_vector.coeff_frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (n : ) :
theorem witt_vector.ghost_component_frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ) (x : R) :
@[instance]
def witt_vector.frobenius_is_poly.comp_i (p : ) [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : , (λ (R : Type u_1) (_Rcr : , witt_vector.frobenius) R _Rcr f)
@[instance]
def witt_vector.frobenius_is_poly.comp₂_i (p : ) [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : (x y : R), (λ (R : Type u_1) (_Rcr : , witt_vector.frobenius) R _Rcr (f x y))
theorem witt_vector.frobenius_is_poly (p : ) [hp : fact (nat.prime p)] :
(λ (R : Type u_1) (_Rcr : , witt_vector.frobenius)

frobenius is tautologically a polynomial function.

@[simp]
theorem witt_vector.coeff_frobenius_char_p (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x : R) (n : ) :
= x.coeff n ^ p
theorem witt_vector.frobenius_eq_map_frobenius (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] :
@[simp]
theorem witt_vector.frobenius_zmodp (p : ) [hp : fact (nat.prime p)] (x : (zmod p)) :
@[simp]
theorem witt_vector.frobenius_equiv_symm_apply (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] [ p] :
noncomputable def witt_vector.frobenius_equiv (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] [ p] :
R ≃+* R

witt_vector.frobenius as an equiv.

Equations
@[simp]
theorem witt_vector.frobenius_equiv_apply (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] [ p] :
theorem witt_vector.frobenius_bijective (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] [ p] :