# mathlibdocumentation

ring_theory.witt_vector.isocrystal

## 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 witt_vector.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.

## Main declarations #

• witt_vector.isocrystal: a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.
• witt_vector.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): fraction_ring (witt_vector p k)
• φ(p, k): witt_vector.fraction_ring.frobenius_ring_hom p k
• M →ᶠˡ[p, k] M₂: linear_map (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂
• M ≃ᶠˡ[p, k] M₂: linear_equiv (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂
• Φ(p, k): witt_vector.isocrystal.frobenius p k
• M →ᶠⁱ[p, k] M₂: witt_vector.isocrystal_hom p k M M₂
• M ≃ᶠⁱ[p, k] M₂: witt_vector.isocrystal_equiv p k M M₂