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 fieldK(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
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 #
- smul : FractionRing (WittVector p k) → V → V
- 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_1 : FractionRing (WittVector p k)) (x : V), (r + s_1) • x = r • x + s_1 • x
- frob : V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V
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
- toFun : V → V₂
- map_add' : ∀ (x y : V), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : FractionRing (WittVector p k)) (x : V), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id (FractionRing (WittVector p k))) r • AddHom.toFun s.toAddHom x
- frob_equivariant : ∀ (x : V), ↑(WittVector.Isocrystal.frobenius p k) (↑s.toLinearMap x) = ↑s.toLinearMap (↑(WittVector.Isocrystal.frobenius p k) x)
A homomorphism between isocrystals respects the Frobenius map.
Instances For
- toFun : V → V₂
- map_add' : ∀ (x y : V), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : FractionRing (WittVector p k)) (x : V), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id (FractionRing (WittVector p k))) r • AddHom.toFun s.toAddHom x
- invFun : V₂ → V
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- frob_equivariant : ∀ (x : V), ↑(WittVector.Isocrystal.frobenius p k) (↑s.toLinearEquiv x) = ↑s.toLinearEquiv (↑(WittVector.Isocrystal.frobenius p k) x)
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
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.