mathlib documentation

ring_theory.witt_vector.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 witt_vector.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.

Main declarations #

Notation #

This file introduces notation in the locale isocrystal.

References #

Frobenius-linear maps #

noncomputable def witt_vector.fraction_ring.frobenius (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] :

The Frobenius automorphism of k induces an automorphism of K.

Equations

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

Equations
Instances for witt_vector.fraction_ring.frobenius_ring_hom

Isocrystals #

@[class]
structure witt_vector.isocrystal (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] (V : Type u_2) [add_comm_group 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 of this typeclass
Instances of other typeclasses for witt_vector.isocrystal
  • witt_vector.isocrystal.has_sizeof_inst

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

Equations
@[nolint]
structure witt_vector.isocrystal_hom (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] (V : Type u_2) [add_comm_group V] [witt_vector.isocrystal p k V] (V₂ : Type u_3) [add_comm_group V₂] [witt_vector.isocrystal p k V₂] :
Type (max u_2 u_3)

A homomorphism between isocrystals respects the Frobenius map.

Instances for witt_vector.isocrystal_hom
  • witt_vector.isocrystal_hom.has_sizeof_inst
@[nolint]
structure witt_vector.isocrystal_equiv (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] (V : Type u_2) [add_comm_group V] [witt_vector.isocrystal p k V] (V₂ : Type u_3) [add_comm_group V₂] [witt_vector.isocrystal p k V₂] :
Type (max u_2 u_3)

An isomorphism between isocrystals respects the Frobenius map.

Instances for witt_vector.isocrystal_equiv
  • witt_vector.isocrystal_equiv.has_sizeof_inst

Classification of isocrystals in dimension 1 #

noncomputable def witt_vector.fraction_ring.module (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] :

A helper instance for type class inference.

Equations
@[nolint]
def witt_vector.standard_one_dim_isocrystal (p : ) [fact (nat.prime p)] (k : Type u_1) [comm_ring 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 witt_vector.standard_one_dim_isocrystal
@[protected, instance]
@[protected, instance]

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