Solving equations about the Frobenius map on the field of fractions of
𝕎 k #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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_polynomial) 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. 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.
- 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+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₂.