mathlib documentation

ring_theory.witt_vector.frobenius_fraction_field

Solving equations about the Frobenius map on the field of fractions of π•Ž k #

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] [char_p k p] (n : β„•) (a₁ aβ‚‚ : witt_vector p 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] [char_p k p] [is_domain k] (n : β„•) (a₁ aβ‚‚ : witt_vector p k) (bs : fin (n + 1) β†’ k) (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
theorem witt_vector.recursion_main.root_exists (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] (n : β„•) (a₁ aβ‚‚ : witt_vector p k) (bs : fin (n + 1) β†’ k) (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
βˆƒ (b : k), (witt_vector.recursion_main.succ_nth_defining_poly p n a₁ aβ‚‚ 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] [char_p k p] [is_alg_closed k] (n : β„•) (a₁ aβ‚‚ : witt_vector p 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
theorem witt_vector.recursion_main.succ_nth_val_spec (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] (n : β„•) (a₁ aβ‚‚ : witt_vector p k) (bs : fin (n + 1) β†’ k) (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
(witt_vector.recursion_main.succ_nth_defining_poly p n a₁ aβ‚‚ bs).is_root (witt_vector.recursion_main.succ_nth_val p n a₁ 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] [char_p k p] [is_alg_closed k] (n : β„•) (a₁ aβ‚‚ : witt_vector p k) (bs : fin (n + 1) β†’ k) (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
witt_vector.recursion_main.succ_nth_val p n a₁ aβ‚‚ bs ha₁ haβ‚‚ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + 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₁) = witt_vector.recursion_main.succ_nth_val p n a₁ aβ‚‚ bs ha₁ haβ‚‚ * aβ‚‚.coeff 0 ^ p ^ (n + 1) + aβ‚‚.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + witt_vector.nth_remainder p n bs (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] [is_alg_closed k] (a₁ aβ‚‚ : witt_vector p 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] [is_alg_closed k] (a₁ aβ‚‚ : witt_vector p 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] [is_alg_closed k] (a₁ aβ‚‚ : witt_vector p k) :
witt_vector.recursion_base.solution p a₁ aβ‚‚ ^ (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] [is_alg_closed k] {a₁ aβ‚‚ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
theorem witt_vector.recursion_base.solution_spec' (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [is_alg_closed k] {a₁ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (aβ‚‚ : witt_vector p k) :
witt_vector.recursion_base.solution p a₁ aβ‚‚ ^ p * a₁.coeff 0 = witt_vector.recursion_base.solution p a₁ aβ‚‚ * aβ‚‚.coeff 0
noncomputable def witt_vector.frobenius_rotation_coeff (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] {a₁ aβ‚‚ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
β„• β†’ k

Recursively defines the sequence of coefficients for witt_vector.frobenius_rotation.

Equations
noncomputable def witt_vector.frobenius_rotation (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] {a₁ aβ‚‚ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  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β‚‚.

Equations
theorem witt_vector.frobenius_rotation_nonzero (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] {a₁ aβ‚‚ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
theorem witt_vector.frobenius_frobenius_rotation (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] {a₁ aβ‚‚ : witt_vector p k} (ha₁ : a₁.coeff 0 β‰  0) (haβ‚‚ : aβ‚‚.coeff 0 β‰  0) :
⇑witt_vector.frobenius (witt_vector.frobenius_rotation p ha₁ haβ‚‚) * a₁ = witt_vector.frobenius_rotation p ha₁ haβ‚‚ * aβ‚‚