Documentation

Mathlib.RingTheory.WittVector.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 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 #

Notation #

This file introduces notation in the locale isocrystal.

References #

Frobenius-linear maps #

The Frobenius automorphism of k induces an automorphism of K.

Instances For

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

    Instances For

      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)

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

      Instances

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

        Instances For
          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)

          A homomorphism between isocrystals respects the Frobenius map.

          Instances For
            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)

            An isomorphism between isocrystals respects the Frobenius map.

            Instances For

              Classification of isocrystals in dimension 1 #

              A helper instance for type class inference.

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

                Instances For

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

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