F-isocrystals over a perfect field

When k is an integral domain, so is 𝕎 k, and we can consider its field of fractions K(p, k). The endomorphism WittVector.frobenius lifts to φ : K(p, k) → K(p, k); if k is perfect, φ is an automorphism.

Let k be a perfect integral domain. Let V be a vector space over K(p,k). An isocrystal is a bijective map V → V that is φ-semilinear. A theorem of Dieudonné and Manin classifies the finite-dimensional isocrystals over algebraically closed fields. In the one-dimensional case, this classification states that the isocrystal structures are parametrized by their "slope" m : ℤ. Any one-dimensional isocrystal is isomorphic to φ(p^m • x) : K(p,k) → K(p,k) for some m.

This file proves this one-dimensional case of the classification theorem. The construction is described in Dupuis, Lewis, and Macbeth, [Formalized functional analysis via semilinear maps][dupuis-lewis-macbeth2022].

Main declarations

• WittVector.Isocrystal: a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.
• WittVector.isocrystal_classification: a one-dimensional isocrystal admits an isomorphism to one of the standard one-dimensional isocrystals.

Notation

This file introduces notation in the scope Isocrystal.

• K(p, k): FractionRing (WittVector p k)
• φ(p, k): WittVector.FractionRing.frobeniusRingHom p k
• M →ᶠˡ[p, k] M₂: LinearMap (WittVector.FractionRing.frobeniusRingHom p k) M M₂
• M ≃ᶠˡ[p, k] M₂: LinearEquiv (WittVector.FractionRing.frobeniusRingHom p k) M M₂
• Φ(p, k): WittVector.Isocrystal.frobenius p k
• M →ᶠⁱ[p, k] M₂: WittVector.IsocrystalHom p k M M₂
• M ≃ᶠⁱ[p, k] M₂: WittVector.IsocrystalEquiv p k M M₂

References

• [Formalized functional analysis via semilinear maps][dupuis-lewis-macbeth2022]
• [Theory of commutative formal groups over fields of finite characteristic][manin1963]
• https://www.math.ias.edu/~lurie/205notes/Lecture26-Isocrystals.pdf

def Isocrystal.«termK(_,_)» : Lean.ParserDescr

The fraction ring of the space of p-Witt vectors on k

Frobenius-linear maps

noncomputable def WittVector.FractionRing.frobenius (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] : FractionRing (WittVector p k) ≃+* FractionRing (WittVector p k)

The Frobenius automorphism of k induces an automorphism of K.

noncomputable def WittVector.FractionRing.frobeniusRingHom (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] : FractionRing (WittVector p k) →+* FractionRing (WittVector p k)

The Frobenius automorphism of k induces an endomorphism of K. For notation purposes. Notation φ(p, k) in the Isocrystal namespace.

def Isocrystal.«termφ(_,_)» : Lean.ParserDescr

The Frobenius automorphism of k induces an endomorphism of K. For notation purposes. Notation φ(p, k) in the Isocrystal namespace.

instance WittVector.inv_pair₁ (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] : RingHomInvPair (FractionRing.frobeniusRingHom p k) ↑(FractionRing.frobenius p k).symm

instance WittVector.inv_pair₂ (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] : RingHomInvPair ↑(FractionRing.frobenius p k).symm ↑(FractionRing.frobenius p k)

def Isocrystal.«term_→ᶠˡ[_,_]_» : Lean.TrailingParserDescr

The Frobenius automorphism of k, as a linear map

def Isocrystal.«term_≃ᶠˡ[_,_]_» : Lean.TrailingParserDescr

The Frobenius automorphism of k, as a linear equivalence

Isocrystals

class WittVector.Isocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] (V : Type u_2) [AddCommGroup V] extends Module (FractionRing (WittVector p k)) V : Type (max u_1 u_2)

An isocrystal is a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.

• smul : FractionRing (WittVector p k) → V → V
• mul_smul (x y : FractionRing (WittVector p k)) (b : V) : (x * y) • b = x • y • b
• one_smul (b : V) : 1 • b = b
• smul_zero (a : FractionRing (WittVector p k)) : a • 0 = 0
• smul_add (a : FractionRing (WittVector p k)) (x y : V) : a • (x + y) = a • x + a • y
• add_smul (r s : FractionRing (WittVector p k)) (x : V) : (r + s) • x = r • x + s • x
• zero_smul (x : V) : 0 • x = 0
• frob : V ≃ₛₗ[FractionRing.frobeniusRingHom p k] V

def WittVector.Isocrystal.frobenius (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] {V : Type u_2} [AddCommGroup V] [Isocrystal p k V] : V ≃ₛₗ[FractionRing.frobeniusRingHom p k] V

Project the Frobenius automorphism from an isocrystal. Denoted by Φ(p, k) when V can be inferred.

def Isocrystal.«termΦ(_,_)» : Lean.ParserDescr

Project the Frobenius automorphism from an isocrystal. Denoted by Φ(p, k) when V can be inferred.

structure WittVector.IsocrystalHom (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] (V : Type u_2) [AddCommGroup V] [Isocrystal p k V] (V₂ : Type u_3) [AddCommGroup V₂] [Isocrystal p k V₂] extends V →ₗ[FractionRing (WittVector p k)] V₂ : Type (max u_2 u_3)

A homomorphism between isocrystals respects the Frobenius map. Notation M →ᶠⁱ [p, k] in the Isocrystal namespace.

• toFun : V → V₂
• map_add' (x y : V) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : FractionRing (WittVector p k)) (x : V) : self.toFun (m • x) = (RingHom.id (FractionRing (WittVector p k))) m • self.toFun x
• frob_equivariant (x : V) : (Isocrystal.frobenius p k) (self.toLinearMap x) = self.toLinearMap ((Isocrystal.frobenius p k) x)

structure WittVector.IsocrystalEquiv (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] [PerfectRing k p] (V : Type u_2) [AddCommGroup V] [Isocrystal p k V] (V₂ : Type u_3) [AddCommGroup V₂] [Isocrystal p k V₂] extends V ≃ₗ[FractionRing (WittVector p k)] V₂ : Type (max u_2 u_3)

An isomorphism between isocrystals respects the Frobenius map.

Notation M ≃ᶠⁱ [p, k] in the Isocrystal namespace.

• toFun : V → V₂
• map_add' (x y : V) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : FractionRing (WittVector p k)) (x : V) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id (FractionRing (WittVector p k))) m • (↑self.toLinearEquiv).toFun x
• invFun : V₂ → V
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• frob_equivariant (x : V) : (Isocrystal.frobenius p k) (self.toLinearEquiv x) = self.toLinearEquiv ((Isocrystal.frobenius p k) x)

def Isocrystal.«term_→ᶠⁱ[_,_]_» : Lean.TrailingParserDescr

A homomorphism between isocrystals respects the Frobenius map. Notation M →ᶠⁱ [p, k] in the Isocrystal namespace.

def Isocrystal.«term_≃ᶠⁱ[_,_]_» : Lean.TrailingParserDescr

An isomorphism between isocrystals respects the Frobenius map.

Notation M ≃ᶠⁱ [p, k] in the Isocrystal namespace.

Classification of isocrystals in dimension 1

def WittVector.StandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] (_m : ℤ) : Type u_1

Type synonym for K(p, k) to carry the standard 1-dimensional isocrystal structure of slope m : ℤ.

@[implicit_reducible]

noncomputable instance WittVector.instAddCommGroupStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] (_m : ℤ) : AddCommGroup (StandardOneDimIsocrystal p k _m)

@[implicit_reducible]

noncomputable instance WittVector.instModuleFractionRingStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] (_m : ℤ) : Module (FractionRing (WittVector p k)) (StandardOneDimIsocrystal p k _m)

@[implicit_reducible]

noncomputable instance WittVector.instIsocrystalStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] (m : ℤ) : Isocrystal p k (StandardOneDimIsocrystal p k m)

The standard one-dimensional isocrystal of slope m : ℤ is an isocrystal.

@[simp]

theorem WittVector.StandardOneDimIsocrystal.frobenius_apply (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] (m : ℤ) (x : StandardOneDimIsocrystal p k m) : (Isocrystal.frobenius p k) x = ↑p ^ m • (FractionRing.frobeniusRingHom p k) x

theorem WittVector.isocrystal_classification (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_2) [Field k] [IsAlgClosed k] [CharP k p] (V : Type u_3) [AddCommGroup V] [Isocrystal p k V] (h_dim : Module.finrank (FractionRing (WittVector p k)) V = 1) : ∃ (m : ℤ), Nonempty (IsocrystalEquiv p k (StandardOneDimIsocrystal p k m) V)

A one-dimensional isocrystal over an algebraically closed field admits an isomorphism to one of the standard (indexed by m : ℤ) one-dimensional isocrystals.