mathlib3 documentation

ring_theory.witt_vector.frobenius

The Frobenius operator #

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

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 #

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 : ) :
witt_vector.frobenius_poly_aux p n = mv_polynomial.X (n + 1) - (finset.range n).sum (λ (i : ), (finset.range (p ^ (n - i))).sum (λ (j : ), (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, _⟩))))
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.

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

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

Equations
Instances for 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 : comm_ring R], witt_vector p R witt_vector p R) [hf : witt_vector.is_poly p f] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), (λ (R : Type u_1) (_Rcr : comm_ring R), 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 : comm_ring R], witt_vector p R witt_vector p R witt_vector p R) [hf : witt_vector.is_poly₂ p f] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.frobenius_fun) R _Rcr (f x y))
noncomputable def witt_vector.frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring 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
@[instance]
def witt_vector.frobenius_is_poly.comp_i (p : ) [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R witt_vector p R) [hf : witt_vector.is_poly p f] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), (λ (R : Type u_1) (_Rcr : comm_ring R), 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 : comm_ring R], witt_vector p R witt_vector p R witt_vector p R) [hf : witt_vector.is_poly₂ p f] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.frobenius) R _Rcr (f x y))

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] [char_p R p] (x : witt_vector p R) (n : ) :
@[simp]