mathlib3 documentation

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] [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) :
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) :
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) :
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) :

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) :