# mathlib3documentation

ring_theory.witt_vector.frobenius_fraction_field

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

noncomputable def witt_vector.recursion_main.succ_nth_defining_poly (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [ p] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) :

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

Equations
theorem witt_vector.recursion_main.succ_nth_defining_poly_degree (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [ p] [is_domain k] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
bs).degree = p
theorem witt_vector.recursion_main.root_exists (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
(b : k), bs).is_root b
noncomputable def witt_vector.recursion_main.succ_nth_val (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
k

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

Equations
• bs ha₁ ha₂ =
theorem witt_vector.recursion_main.succ_nth_val_spec (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
bs).is_root a₂ bs ha₁ ha₂)
theorem witt_vector.recursion_main.succ_nth_val_spec' (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] (n : ) (a₁ a₂ : k) (bs : fin (n + 1) k) (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + (λ (v : fin (n + 1)), bs v ^ p) (witt_vector.truncate_fun (n + 1) a₁) = bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + (witt_vector.truncate_fun (n + 1) a₂)
theorem witt_vector.recursion_base.solution_pow (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] (a₁ a₂ : k) :
(x : k), x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
noncomputable def witt_vector.recursion_base.solution (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] (a₁ a₂ : k) :
k

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

Equations
theorem witt_vector.recursion_base.solution_spec (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] (a₁ a₂ : k) :
^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
theorem witt_vector.recursion_base.solution_nonzero (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] {a₁ a₂ : k} (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
0
theorem witt_vector.recursion_base.solution_spec' (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] {a₁ : k} (ha₁ : a₁.coeff 0 0) (a₂ : k) :
^ p * a₁.coeff 0 = * a₂.coeff 0
noncomputable def witt_vector.frobenius_rotation_coeff (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] {a₁ a₂ : k} (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :

Recursively defines the sequence of coefficients for witt_vector.frobenius_rotation.

Equations
• ha₂ (n + 1) = (λ (i : fin (n + 1)), ha₂ i.val) ha₁ ha₂
• ha₂ 0 =
noncomputable def witt_vector.frobenius_rotation (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] {a₁ a₂ : k} (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
k

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
theorem witt_vector.frobenius_rotation_nonzero (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] {a₁ a₂ : k} (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
ha₂ 0
theorem witt_vector.frobenius_frobenius_rotation (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] {a₁ a₂ : k} (ha₁ : a₁.coeff 0 0) (ha₂ : a₂.coeff 0 0) :
* a₁ = ha₂ * a₂
theorem witt_vector.exists_frobenius_solution_fraction_ring_aux (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] (m n : ) (r' q' : k) (hr' : r'.coeff 0 0) (hq' : q'.coeff 0 0) (hq : p ^ n * q' ) :
let b : k := hq' in ((algebra_map k) (fraction_ring k))) b) * localization.mk (p ^ m * r') p ^ n * q', hq⟩ = p ^ (m - n) * (algebra_map k) (fraction_ring k))) b
theorem witt_vector.exists_frobenius_solution_fraction_ring (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [ p] {a : fraction_ring k)} (ha : a 0) :
(b : fraction_ring k)) (hb : b 0) (m : ), = p ^ m * b