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 #

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.