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 locale 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

Frobenius-linear maps

def WittVector.FractionRing.frobenius (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain 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.

def WittVector.FractionRing.frobeniusRingHom (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain 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.

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

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

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

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

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

Isocrystals

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

• smul : FractionRing (WittVector p k) → V → V
• one_smul : ∀ (b : V), 1 • b = b
• mul_smul : ∀ (x y : FractionRing (WittVector p k)) (b : V), (x * y) • b = x • y • 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_1 : FractionRing (WittVector p k)) (x : V), (r + s_1) • x = r • x + s_1 • x
• zero_smul : ∀ (x : V), 0 • x = 0
• frob : V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V

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

def WittVector.Isocrystal.frobenius (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] {V : Type u_2} [AddCommGroup V] [WittVector.Isocrystal p k V] : V ≃ₛₗ[WittVector.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

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

• toFun : V → V₂
• map_add' : ∀ (x y : V), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : FractionRing (WittVector p k)) (x : V), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id (FractionRing (WittVector p k))) r • AddHom.toFun s.toAddHom x
• frob_equivariant : ∀ (x : V), ↑(WittVector.Isocrystal.frobenius p k) (↑s.toLinearMap x) = ↑s.toLinearMap (↑(WittVector.Isocrystal.frobenius p k) x)

A homomorphism between isocrystals respects the Frobenius map.

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

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

An isomorphism between isocrystals respects the Frobenius map.

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

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

Classification of isocrystals in dimension 1

def WittVector.FractionRing.module (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] : Module (FractionRing (WittVector p k)) (FractionRing (WittVector p k))

A helper instance for type class inference.

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 : ℤ.

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

instance WittVector.instModuleFractionRingWittVectorInstCommRingWittVectorStandardOneDimIsocrystalToSemiringInstCommSemiringLocalizationToCommMonoidToCommSemiringNonZeroDivisorsToMonoidWithZeroToAddCommMonoidInstAddCommGroupStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] {m : ℤ} : Module (FractionRing (WittVector p k)) (WittVector.StandardOneDimIsocrystal p k m)

instance WittVector.instIsocrystalStandardOneDimIsocrystalInstAddCommGroupStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] (m : ℤ) : WittVector.Isocrystal p k (WittVector.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 : WittVector.StandardOneDimIsocrystal p k m) : ↑(WittVector.Isocrystal.frobenius p k) x = ↑p ^ m • ↑(WittVector.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] [WittVector.Isocrystal p k V] (h_dim : FiniteDimensional.finrank (FractionRing (WittVector p k)) V = 1) : ∃ m, Nonempty (WittVector.IsocrystalEquiv p k (WittVector.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.