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

• smul : FractionRing (WittVector p k) → V → V
• one_smul : ∀ (b : V), 1 • b = b
• mul_smul : ∀ (x y : FractionRing (WittVector p k)) (b : V), (x * y) • b = x • y • b
• smul_zero : ∀ (a : FractionRing (WittVector p k)), a • 0 = 0
• smul_add : ∀ (a : FractionRing (WittVector p k)) (x y : V), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : FractionRing (WittVector p k)) (x : V), (r + s) • x = r • x + s • x
• zero_smul : ∀ (x : V), 0 • x = 0
• frob : V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V

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

A homomorphism between isocrystals respects the Frobenius map.

• toFun : V → V₂
• map_add' : ∀ (x y : V), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (m : FractionRing (WittVector p k)) (x : V), self.toFun (m • x) = (RingHom.id (FractionRing (WittVector p k))) m • self.toFun x
• frob_equivariant : ∀ (x : V), (WittVector.Isocrystal.frobenius p k) (self.toLinearMap x) = self.toLinearMap ((WittVector.Isocrystal.frobenius p k) x)

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

An isomorphism between isocrystals respects the Frobenius map.

• toFun : V → V₂
• map_add' : ∀ (x y : V), (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' : ∀ (m : FractionRing (WittVector p k)) (x : V), (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id (FractionRing (WittVector p k))) m • (↑self.toLinearEquiv).toFun x
• invFun : V₂ → V
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• frob_equivariant : ∀ (x : V), (WittVector.Isocrystal.frobenius p k) (self.toLinearEquiv x) = self.toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)

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 : FiniteDimensional.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.