Documentation

Mathlib.RingTheory.WittVector.FrobeniusFractionField

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

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.
Instances For
    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) :
    (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).degree = ↑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), (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot 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
    Instances For
      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.succNthDefiningPoly p n a₁ a₂ bs).IsRoot (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
      Instances For
        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) :
        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
        Instances For
          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) :

          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
          Instances For
            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') ⟨↑p ^ n * q', 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