# Documentation

Mathlib.RingTheory.WittVector.FrobeniusFractionField

# Solving equations about the Frobenius map on the field of fractions of 𝕎 k#

The goal of this file is to prove WittVector.exists_frobenius_solution_fractionRing, 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 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 (WittVector.wittMul, wittPolynomial) to show that they satisfy the desired equation.

Preliminary work is done in the dependency RingTheory.WittVector.MulCoeff 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][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 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.

def WittVector.RecursionMain.succNthDefiningPoly (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) :

The root of this polynomial determines the n+1st coefficient of our solution.

Instances For
theorem WittVector.RecursionMain.succNthDefiningPoly_degree (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) (ha₁ : 0) (ha₂ : 0) :
= p
theorem WittVector.RecursionMain.root_exists (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) (ha₁ : 0) (ha₂ : 0) :
b, Polynomial.IsRoot () b
def WittVector.RecursionMain.succNthVal (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) (ha₁ : 0) (ha₂ : 0) :
k

This is the n+1st coefficient of our solution, projected from root_exists.

Instances For
theorem WittVector.RecursionMain.succNthVal_spec (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) (ha₁ : 0) (ha₂ : 0) :
Polynomial.IsRoot () (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)
theorem WittVector.RecursionMain.succNthVal_spec' (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (n : ) (a₁ : ) (a₂ : ) (bs : Fin (n + 1)k) (ha₁ : 0) (ha₂ : 0) :
WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * ^ p ^ (n + 1) + WittVector.coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + WittVector.nthRemainder p n (fun v => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) = WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ * ^ p ^ (n + 1) + WittVector.coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) + WittVector.nthRemainder p n bs (WittVector.truncateFun (n + 1) a₂)
theorem WittVector.RecursionBase.solution_pow (p : ) [hp : Fact ()] {k : Type u_1} [] [] (a₁ : ) (a₂ : ) :
x, x ^ (p - 1) = /
def WittVector.RecursionBase.solution (p : ) [hp : Fact ()] {k : Type u_1} [] [] (a₁ : ) (a₂ : ) :
k

The base case (0th coefficient) of our solution vector.

Instances For
theorem WittVector.RecursionBase.solution_spec (p : ) [hp : Fact ()] {k : Type u_1} [] [] (a₁ : ) (a₂ : ) :
^ (p - 1) = /
theorem WittVector.RecursionBase.solution_nonzero (p : ) [hp : Fact ()] {k : Type u_1} [] [] {a₁ : } {a₂ : } (ha₁ : 0) (ha₂ : 0) :
0
theorem WittVector.RecursionBase.solution_spec' (p : ) [hp : Fact ()] {k : Type u_1} [] [] {a₁ : } (ha₁ : 0) (a₂ : ) :
^ p * = *
noncomputable def WittVector.frobeniusRotationCoeff (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] {a₁ : } {a₂ : } (ha₁ : 0) (ha₂ : 0) :
k

Recursively defines the sequence of coefficients for WittVector.frobeniusRotation.

Equations
Instances For
def WittVector.frobeniusRotation (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] {a₁ : } {a₂ : } (ha₁ : 0) (ha₂ : 0) :

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₂.

Instances For
theorem WittVector.frobeniusRotation_nonzero (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] {a₁ : } {a₂ : } (ha₁ : 0) (ha₂ : 0) :
theorem WittVector.frobenius_frobeniusRotation (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] {a₁ : } {a₂ : } (ha₁ : 0) (ha₂ : 0) :
WittVector.frobenius (WittVector.frobeniusRotation p ha₁ ha₂) * a₁ = WittVector.frobeniusRotation p ha₁ ha₂ * a₂
theorem WittVector.exists_frobenius_solution_fractionRing_aux (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] (m : ) (n : ) (r' : ) (q' : ) (hr' : 0) (hq' : 0) (hq : p ^ n * q' ) :
let b := WittVector.frobeniusRotation p hr' hq'; ↑() (↑(algebraMap () (FractionRing ())) b) * Localization.mk (p ^ m * r') { val := p ^ n * q', property := hq } = p ^ (m - n) * ↑(algebraMap () (FractionRing ())) b
theorem WittVector.exists_frobenius_solution_fractionRing (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] [] {a : FractionRing ()} (ha : a 0) :
b hb m, = p ^ m * b