# Documentation

## 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]
Equations
• One or more equations did not get rendered due to their size.
Instances For

### Frobenius-linear maps #

def WittVector.FractionRing.frobenius (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] :

The Frobenius automorphism of k induces an automorphism of K.

Equations
Instances For
def WittVector.FractionRing.frobeniusRingHom (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] :

The Frobenius automorphism of k induces an endomorphism of K. For notation purposes.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
instance WittVector.inv_pair₁ (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] :
Equations
• =
instance WittVector.inv_pair₂ (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] :
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

### Isocrystals #

class WittVector.Isocrystal (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] (V : Type u_2) [] extends :
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.

Instances
def WittVector.Isocrystal.frobenius (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] {V : Type u_2} [] [] :

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

Equations
• = WittVector.Isocrystal.frob
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
structure WittVector.IsocrystalHom (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] (V : Type u_2) [] [] (V₂ : Type u_3) [] [] extends :
Type (max u_2 u_3)

A homomorphism between isocrystals respects the Frobenius map.

• toFun : VV₂
• map_add' : ∀ (x y : V), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (m : FractionRing ()) (x : V), self.toFun (m x) = (RingHom.id (FractionRing ())) m self.toFun x
• frob_equivariant : ∀ (x : V), (self.toLinearMap x) = self.toLinearMap ()
Instances For
theorem WittVector.IsocrystalHom.frob_equivariant {p : } [Fact p.Prime] {k : Type u_1} [] [] [CharP k p] [] {V : Type u_2} [] [] {V₂ : Type u_3} [] [] (self : ) (x : V) :
(self.toLinearMap x) = self.toLinearMap ()
structure WittVector.IsocrystalEquiv (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] (V : Type u_2) [] [] (V₂ : Type u_3) [] [] extends :
Type (max u_2 u_3)

An isomorphism between isocrystals respects the Frobenius map.

Instances For
theorem WittVector.IsocrystalEquiv.frob_equivariant {p : } [Fact p.Prime] {k : Type u_1} [] [] [CharP k p] [] {V : Type u_2} [] [] {V₂ : Type u_3} [] [] (self : ) (x : V) :
(self.toLinearEquiv x) = self.toLinearEquiv ()
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

### Classification of isocrystals in dimension 1 #

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

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

Equations
Instances For
instance WittVector.instAddCommGroupStandardOneDimIsocrystal (p : ) [Fact p.Prime] (k : Type u_1) [] {m : } :
Equations
Equations
instance WittVector.instIsocrystalStandardOneDimIsocrystal (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] (m : ) :

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WittVector.StandardOneDimIsocrystal.frobenius_apply (p : ) [Fact p.Prime] (k : Type u_1) [] [] [CharP k p] [] (m : ) (x : ) :
= p ^ m
theorem WittVector.isocrystal_classification (p : ) [Fact p.Prime] (k : Type u_2) [] [] [CharP k p] (V : Type u_3) [] [] (h_dim : = 1) :
∃ (m : ),

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