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 (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) : Polynomial k

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

theorem WittVector.RecursionMain.succNthDefiningPoly_degree (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [IsDomain k] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : Polynomial.degree (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs) = ↑p

theorem WittVector.RecursionMain.root_exists (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : ∃ b, Polynomial.IsRoot (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs) b

def WittVector.RecursionMain.succNthVal (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : k

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

theorem WittVector.RecursionMain.succNthVal_spec (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : Polynomial.IsRoot (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs) (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)

theorem WittVector.RecursionMain.succNthVal_spec' (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ : WittVector p k) (a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * WittVector.coeff a₁ 0 ^ 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₂ * WittVector.coeff a₂ 0 ^ 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 (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ : WittVector p k) (a₂ : WittVector p k) : ∃ x, x ^ (p - 1) = WittVector.coeff a₂ 0 / WittVector.coeff a₁ 0

def WittVector.RecursionBase.solution (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ : WittVector p k) (a₂ : WittVector p k) : k

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

theorem WittVector.RecursionBase.solution_spec (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ : WittVector p k) (a₂ : WittVector p k) : WittVector.RecursionBase.solution p a₁ a₂ ^ (p - 1) = WittVector.coeff a₂ 0 / WittVector.coeff a₁ 0

theorem WittVector.RecursionBase.solution_nonzero (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] {a₁ : WittVector p k} {a₂ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : WittVector.RecursionBase.solution p a₁ a₂ ≠ 0

theorem WittVector.RecursionBase.solution_spec' (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] {a₁ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (a₂ : WittVector p k) : WittVector.RecursionBase.solution p a₁ a₂ ^ p * WittVector.coeff a₁ 0 = WittVector.RecursionBase.solution p a₁ a₂ * WittVector.coeff a₂ 0

noncomputable def WittVector.frobeniusRotationCoeff (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ : WittVector p k} {a₂ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : ℕ → k

Recursively defines the sequence of coefficients for WittVector.frobeniusRotation.

Equations

• WittVector.frobeniusRotationCoeff p ha₁ ha₂ 0 = WittVector.RecursionBase.solution p a₁ a₂
• WittVector.frobeniusRotationCoeff p ha₁ ha₂ (Nat.succ n) = WittVector.RecursionMain.succNthVal p n a₁ a₂ (fun i => WittVector.frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂

def WittVector.frobeniusRotation (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ : WittVector p k} {a₂ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : WittVector 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₂.

theorem WittVector.frobeniusRotation_nonzero (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ : WittVector p k} {a₂ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 0) : WittVector.frobeniusRotation p ha₁ ha₂ ≠ 0

theorem WittVector.frobenius_frobeniusRotation (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ : WittVector p k} {a₂ : WittVector p k} (ha₁ : WittVector.coeff a₁ 0 ≠ 0) (ha₂ : WittVector.coeff a₂ 0 ≠ 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 (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (m : ℕ) (n : ℕ) (r' : WittVector p k) (q' : WittVector p k) (hr' : WittVector.coeff r' 0 ≠ 0) (hq' : WittVector.coeff q' 0 ≠ 0) (hq : ↑p ^ n * q' ∈ nonZeroDivisors (WittVector p k)) : let b := WittVector.frobeniusRotation p hr' hq'; ↑(IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) (↑(algebraMap (WittVector p k) (FractionRing (WittVector p k))) b) * Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } = ↑p ^ (↑m - ↑n) * ↑(algebraMap (WittVector p k) (FractionRing (WittVector p k))) b

theorem WittVector.exists_frobenius_solution_fractionRing (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a : FractionRing (WittVector p k)} (ha : a ≠ 0) : ∃ b hb m, ↑(IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b