WittVector.isocrystal_classification

theorem WittVector.isocrystal_classification : ∀ (p : ℕ) [inst : Fact p.Prime] (k : Type u_2) [inst_1 : Field k] [inst_2 : IsAlgClosed k] [inst_3 : CharP k p] (V : Type u_3) [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V], FiniteDimensional.finrank (FractionRing (WittVector p k)) V = 1 → ∃ m, Nonempty (WittVector.IsocrystalEquiv p k (WittVector.StandardOneDimIsocrystal p k m) V)

This theorem, known as `WittVector.isocrystal_classification`, states that given a prime number `p`, and an algebraically closed field `k` of characteristic `p`, for any one-dimensional isocrystal `V` over this field, there exists an integer `m` such that `V` is isomorphic to the standard one-dimensional isocrystal of slope `m`. Here, an isocrystal is said to be one-dimensional if the rank of the module over the fraction ring of the Witt vector ring is one. In other words, this theorem provides a classification for one-dimensional isocrystals over an algebraically closed field in terms of the standard isocrystals.

More concisely: Given a prime number p and an algebraically closed field k of characteristic p, every one-dimensional isocrystal V over k is isomorphic to a standard one-dimensional isocrystal of some integer slope.