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 #

The fraction ring of the space of p-Witt vectors on k

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Frobenius-linear maps #

    The Frobenius automorphism of k induces an automorphism of K.

    Equations
    Instances For

      The Frobenius automorphism of k induces an endomorphism of K. For notation purposes. Notation φ(p, k) in the Isocrystal namespace.

      Equations
      Instances For

        The Frobenius automorphism of k induces an endomorphism of K. For notation purposes. Notation φ(p, k) in the Isocrystal namespace.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The Frobenius automorphism of k, as a linear map

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Pretty printer defined by notation3 command.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The Frobenius automorphism of k, as a linear equivalence

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Isocrystals #

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

                    Equations
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        structure WittVector.IsocrystalHom (p : ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing 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 V →ₗ[FractionRing (WittVector p k)] V₂ :
                        Type (max u_2 u_3)

                        A homomorphism between isocrystals respects the Frobenius map. Notation M →ᶠⁱ [p, k] in the Isocrystal namespace.

                        Instances For
                          structure WittVector.IsocrystalEquiv (p : ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing 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 V ≃ₗ[FractionRing (WittVector p k)] V₂ :
                          Type (max u_2 u_3)

                          An isomorphism between isocrystals respects the Frobenius map.

                          Notation M ≃ᶠⁱ [p, k] in the Isocrystal namespace.

                          Instances For

                            A homomorphism between isocrystals respects the Frobenius map. Notation M →ᶠⁱ [p, k] in the Isocrystal namespace.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              An isomorphism between isocrystals respects the Frobenius map.

                              Notation M ≃ᶠⁱ [p, k] in the Isocrystal namespace.

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

                                Equations
                                Instances For

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

                                  Equations
                                  • One or more equations did not get rendered due to their size.

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