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.

source
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) :
polynomial k

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

Equations
source
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) :
(witt_vector.recursion_main.succ_nth_defining_poly p n a₁ aβ‚‚ bs).degree = ↑p
source
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
source
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
source
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β‚‚)
source
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β‚‚)
source
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
source
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
source
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
source
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) :
witt_vector.recursion_base.solution p a₁ aβ‚‚ β‰  0
source
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
source
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
source
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) :
witt_vector p 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
source
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) :
witt_vector.frobenius_rotation p ha₁ haβ‚‚ β‰  0
source
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β‚‚
source
theorem witt_vector.exists_frobenius_solution_fraction_ring_aux (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] (m n : β„•) (r' q' : witt_vector p k) (hr' : r'.coeff 0 β‰  0) (hq' : q'.coeff 0 β‰  0) (hq : ↑p ^ n * q' ∈ non_zero_divisors (witt_vector p k)) :
let b : witt_vector p k := witt_vector.frobenius_rotation p hr' hq' in ⇑(is_fraction_ring.field_equiv_of_ring_equiv (witt_vector.frobenius_equiv p k)) (⇑(algebra_map (witt_vector p k) (fraction_ring (witt_vector p k))) b) * localization.mk (↑p ^ m * r') βŸ¨β†‘p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * ⇑(algebra_map (witt_vector p k) (fraction_ring (witt_vector p k))) b
source
theorem witt_vector.exists_frobenius_solution_fraction_ring (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [is_alg_closed k] {a : fraction_ring (witt_vector p k)} (ha : a β‰  0) :
βˆƒ (b : fraction_ring (witt_vector p k)) (hb : b β‰  0) (m : β„€), ⇑(is_fraction_ring.field_equiv_of_ring_equiv (witt_vector.frobenius_equiv p k)) b * a = ↑p ^ m * b