Solving equations about the Frobenius map on the field of fractions of π k
#
The goal of this file is to prove witt_vector.exists_frobenius_solution_fraction_ring
,
which says that for an algebraically closed field k
of characteristic p
and a, b
in the
field of fractions of Witt vectors over k
,
there is a solution b
to the equation Ο b * a = p ^ m * b
, where Ο
is the Frobenius map.
Most of this file builds up the equivalent theorem over π k
directly,
moving to the field of fractions at the end.
See witt_vector.frobenius_rotation
and its specification.
The construction proceeds by recursively defining a sequence of coefficients as solutions to a
polynomial equation in k
. We must define these as generic polynomials using Witt vector API
(witt_vector.witt_mul
, witt_polynomial
) to show that they satisfy the desired equation.
Preliminary work is done in the dependency ring_theory.witt_vector.mul_coeff
to isolate the n+1
st coefficients of x
and y
in the n+1
st coefficient of x*y
.
This construction is described in Dupuis, Lewis, and Macbeth, Formalized functional analysis via semilinear maps. We approximately follow an approach sketched on MathOverflow: https://mathoverflow.net/questions/62468/about-frobenius-of-witt-vectors
The result is a dependency for the proof of witt_vector.isocrystal_classification
,
the classification of one-dimensional isocrystals over an algebraically closed field.
The recursive case of the vector coefficients #
The first coefficient of our solution vector is easy to define below.
In this section we focus on the recursive case.
The goal is to turn witt_poly_prod n
into a univariate polynomial
whose variable represents the n
th coefficient of x
in x * a
.
The root of this polynomial determines the n+1
st coefficient of our solution.
Equations
- witt_vector.recursion_main.succ_nth_defining_poly p n aβ aβ bs = polynomial.X ^ p * βpolynomial.C (aβ.coeff 0 ^ p ^ (n + 1)) - polynomial.X * βpolynomial.C (aβ.coeff 0 ^ p ^ (n + 1)) + βpolynomial.C (aβ.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + witt_vector.nth_remainder p n (Ξ» (v : fin (n + 1)), bs v ^ p) (witt_vector.truncate_fun (n + 1) aβ) - aβ.coeff (n + 1) * bs 0 ^ p ^ (n + 1) - witt_vector.nth_remainder p n bs (witt_vector.truncate_fun (n + 1) aβ))
This is the n+1
st coefficient of our solution, projected from root_exists
.
Equations
- witt_vector.recursion_main.succ_nth_val p n aβ aβ bs haβ haβ = classical.some _
The base case (0th coefficient) of our solution vector.
Equations
- witt_vector.recursion_base.solution p aβ aβ = classical.some _
Recursively defines the sequence of coefficients for witt_vector.frobenius_rotation
.
Equations
- witt_vector.frobenius_rotation_coeff p haβ haβ (n + 1) = witt_vector.recursion_main.succ_nth_val p n aβ aβ (Ξ» (i : fin (n + 1)), witt_vector.frobenius_rotation_coeff p haβ haβ i.val) haβ haβ
- witt_vector.frobenius_rotation_coeff p haβ haβ 0 = witt_vector.recursion_base.solution p aβ aβ
For nonzero aβ
and aβ
, frobenius_rotation aβ aβ
is a Witt vector that satisfies the
equation frobenius (frobenius_rotation aβ aβ) * aβ = (frobenius_rotation aβ aβ) * aβ
.
Equations
- witt_vector.frobenius_rotation p haβ haβ = {coeff := witt_vector.frobenius_rotation_coeff p haβ haβ}