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 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+1st coefficients of x and y in the n+1st 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 nth coefficient of x in x * a.