Solving equations about the Frobenius map on the field of fractions of
𝕎 k #
The goal of this file is to prove
which says that for an algebraically closed field
k of characteristic
a, b in the
field of fractions of Witt vectors over
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.
WittVector.frobeniusRotation 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
wittPolynomial) to show that they satisfy the desired equation.
Preliminary work is done in the dependency
to isolate the
n+1st coefficients of
y in the
n+1st coefficient of
This construction is described in Dupuis, Lewis, and Macbeth, [Formalized functional analysis via semilinear maps][dupuis-lewis-macbeth2022]. 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
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
nth coefficient of
x * a.
The root of this polynomial determines the
n+1st coefficient of our solution.
This is the
n+1st coefficient of our solution, projected from
Recursively defines the sequence of coefficients for
frobenius_rotation a₁ a₂ is a Witt vector that satisfies the
frobenius (frobenius_rotation a₁ a₂) * a₁ = (frobenius_rotation a₁ a₂) * a₂.