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 offrobenius_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 characteristicp
, Frobenius is equal towitt_vector.map (frobenius R p)
.
TODO: Show that witt_vector.frobenius_fun
is a ring homomorphism,
and bundle it into witt_vector.frobenius
.
References #
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)
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, _⟩))
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
A key numerical identity needed for the proof of witt_vector.map_frobenius_poly
.
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))
frobenius_fun
is tautologically a polynomial function.
See also frobenius_is_poly
.
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
- witt_vector.frobenius = {to_fun := witt_vector.frobenius_fun _inst_1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
frobenius
is tautologically a polynomial function.