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

• WittVector.Isocrystal: a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.
• WittVector.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): FractionRing (WittVector p k)
• φ(p, k): WittVector.FractionRing.frobeniusRingHom p k
• M →ᶠˡ[p, k] M₂: LinearMap (WittVector.FractionRing.frobeniusRingHom p k) M M₂
• M ≃ᶠˡ[p, k] M₂: LinearEquiv (WittVector.FractionRing.frobeniusRingHom p k) M M₂
• Φ(p, k): WittVector.Isocrystal.frobenius p k
• M →ᶠⁱ[p, k] M₂: WittVector.IsocrystalHom p k M M₂
• M ≃ᶠⁱ[p, k] M₂: WittVector.IsocrystalEquiv p k M M₂

References

• [Formalized functional analysis via semilinear maps][dupuis-lewis-macbeth2022]
• [Theory of commutative formal groups over fields of finite characteristic][manin1963]
• https://www.math.ias.edu/~lurie/205notes/Lecture26-Isocrystals.pdf

def Isocrystal.«termK(_,_)» : Lean.ParserDescr

Equations

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

Frobenius-linear maps

def WittVector.FractionRing.frobenius (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] : FractionRing (WittVector p k) ≃+* FractionRing (WittVector p k)

The Frobenius automorphism of k induces an automorphism of K.

Equations

• WittVector.FractionRing.frobenius p k = IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)

def WittVector.FractionRing.frobeniusRingHom (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] : FractionRing (WittVector p k) →+* FractionRing (WittVector p k)

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

Equations

• WittVector.FractionRing.frobeniusRingHom p k = ↑(WittVector.FractionRing.frobenius p k)

def Isocrystal.«termφ(_,_)» : Lean.ParserDescr

Equations

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

instance WittVector.inv_pair₁ (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] : RingHomInvPair (WittVector.FractionRing.frobeniusRingHom p k) ↑(WittVector.FractionRing.frobenius p k).symm

Equations

• ⋯ = ⋯

instance WittVector.inv_pair₂ (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] : RingHomInvPair ↑(WittVector.FractionRing.frobenius p k).symm ↑(WittVector.FractionRing.frobenius p k)

Equations

• ⋯ = ⋯

def Isocrystal.«term_→ᶠˡ[_,_]_» : Lean.TrailingParserDescr

Equations

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

def Isocrystal.«term_≃ᶠˡ[_,_]_» : Lean.TrailingParserDescr

Equations

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

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 , DistribMulAction , MulAction , SMul : 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.

def WittVector.Isocrystal.frobenius (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 ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V

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

Equations

• WittVector.Isocrystal.frobenius p k = WittVector.Isocrystal.frob

def Isocrystal.«termΦ(_,_)» : Lean.ParserDescr

Equations

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

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 , AddHom , MulActionHom : Type (max u_2 u_3)

A homomorphism between isocrystals respects the Frobenius map.

theorem WittVector.IsocrystalHom.frob_equivariant {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₂] (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 (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 , LinearMap , AddEquiv , Equiv , AddHom , MulActionHom : Type (max u_2 u_3)

An isomorphism between isocrystals respects the Frobenius map.

theorem WittVector.IsocrystalEquiv.frob_equivariant {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₂] (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)

def Isocrystal.«term_→ᶠⁱ[_,_]_» : Lean.TrailingParserDescr

Equations

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

def Isocrystal.«term_≃ᶠⁱ[_,_]_» : Lean.TrailingParserDescr

Equations

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

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

• WittVector.StandardOneDimIsocrystal p k _m = FractionRing (WittVector p k)

instance WittVector.instAddCommGroupStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] {m : ℤ} : AddCommGroup (WittVector.StandardOneDimIsocrystal p k m)

Equations

• WittVector.instAddCommGroupStandardOneDimIsocrystal p k = inferInstanceAs (AddCommGroup (FractionRing (WittVector p k)))

instance WittVector.instModuleFractionRingStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] {m : ℤ} : Module (FractionRing (WittVector p k)) (WittVector.StandardOneDimIsocrystal p k m)

Equations

• WittVector.instModuleFractionRingStandardOneDimIsocrystal p k = inferInstanceAs (Module (FractionRing (WittVector p k)) (FractionRing (WittVector p k)))

instance WittVector.instIsocrystalStandardOneDimIsocrystal (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] (m : ℤ) : WittVector.Isocrystal p k (WittVector.StandardOneDimIsocrystal p k m)

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

Equations

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

@[simp]

theorem WittVector.StandardOneDimIsocrystal.frobenius_apply (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_1) [CommRing k] [IsDomain k] [CharP k p] [PerfectRing k p] (m : ℤ) (x : WittVector.StandardOneDimIsocrystal p k m) : (WittVector.Isocrystal.frobenius p k) x = ↑p ^ m • (WittVector.FractionRing.frobeniusRingHom p k) x

theorem WittVector.isocrystal_classification (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_2) [Field k] [IsAlgClosed k] [CharP k p] (V : Type u_3) [AddCommGroup V] [WittVector.Isocrystal p k V] (h_dim : Module.finrank (FractionRing (WittVector p k)) V = 1) : ∃ (m : ℤ), Nonempty (WittVector.IsocrystalEquiv p k (WittVector.StandardOneDimIsocrystal p k m) V)

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