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:

The result is a dependency for the proof of WittVector.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 WittVector.wittPolyProd 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.

Equations

• One or more equations did not get rendered due to their size.

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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ∃ (b : k), 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : k

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

Equations

• WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ = Classical.choose ⋯

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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + WittVector.nthRemainder p n (fun (v : Fin (n + 1)) => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) = WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (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 : k), x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 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.

Equations

• WittVector.RecursionBase.solution p a₁ a₂ = Classical.choose ⋯

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) = a₂.coeff 0 / a₁.coeff 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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₁ : a₁.coeff 0 ≠ 0) (a₂ : WittVector p k) : WittVector.RecursionBase.solution p a₁ a₂ ^ p * a₁.coeff 0 = WittVector.RecursionBase.solution p a₁ a₂ * a₂.coeff 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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 : Fin (n + 1)) => 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector p k

For nonzero a₁ and a₂, frobeniusRotation a₁ a₂ is a Witt vector that satisfies the equation frobenius (frobeniusRotation a₁ a₂) * a₁ = (frobeniusRotation a₁ a₂) * a₂.

Equations

• WittVector.frobeniusRotation p ha₁ ha₂ = WittVector.mk p (WittVector.frobeniusRotationCoeff p ha₁ ha₂)

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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 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' : r'.coeff 0 ≠ 0) (hq' : q'.coeff 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 : FractionRing (WittVector p k)), b ≠ 0 ∧ ∃ (m : ℤ), (IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b