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 #

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.

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

                Equations
                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) [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
                      theorem WittVector.IsocrystalHom.frob_equivariant {p : } [Fact p.Prime] {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₂] (self : WittVector.IsocrystalHom p k V V₂) (x : V) :
                      (WittVector.Isocrystal.frobenius p k) (self.toLinearMap x) = self.toLinearMap ((WittVector.Isocrystal.frobenius p k) x)
                      structure WittVector.IsocrystalEquiv (p : ) [Fact p.Prime] (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
                        theorem WittVector.IsocrystalEquiv.frob_equivariant {p : } [Fact p.Prime] {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₂] (self : WittVector.IsocrystalEquiv p k V V₂) (x : V) :
                        (WittVector.Isocrystal.frobenius p k) (self.toLinearEquiv x) = self.toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)
                        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) [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.