mathlib3 documentation

ring_theory.witt_vector.isocrystal

F-isocrystals over a perfect field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

witt_vector.isocrystal: a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.
witt_vector.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): fraction_ring (witt_vector p k)
φ(p, k): witt_vector.fraction_ring.frobenius_ring_hom p k
M →ᶠˡ[p, k] M₂: linear_map (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂
M ≃ᶠˡ[p, k] M₂: linear_equiv (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂
Φ(p, k): witt_vector.isocrystal.frobenius p k
M →ᶠⁱ[p, k] M₂: witt_vector.isocrystal_hom p k M M₂
M ≃ᶠⁱ[p, k] M₂: witt_vector.isocrystal_equiv p k M M₂

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

fraction_ring (witt_vector p k) ≃+* fraction_ring (witt_vector p k)

The Frobenius automorphism of k induces an automorphism of K.

Equations

witt_vector.fraction_ring.frobenius p k = is_fraction_ring.field_equiv_of_ring_equiv (witt_vector.frobenius_equiv p k)

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

fraction_ring (witt_vector p k) →+* fraction_ring (witt_vector p k)

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

Equations

witt_vector.fraction_ring.frobenius_ring_hom p k = ↑(witt_vector.fraction_ring.frobenius p k)

Instances for witt_vector.fraction_ring.frobenius_ring_hom

witt_vector.inv_pair₁

@[protected, instance]

def witt_vector.inv_pair₁ (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] :

ring_hom_inv_pair (witt_vector.fraction_ring.frobenius_ring_hom p k) ↑((witt_vector.fraction_ring.frobenius p k).symm)

@[protected, instance]

def witt_vector.inv_pair₂ (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] :

ring_hom_inv_pair ↑((witt_vector.fraction_ring.frobenius p k).symm) ↑((witt_vector.fraction_ring.frobenius p k).symm.symm)

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)

to_module : module (fraction_ring (witt_vector p k)) V
frob : V ≃ₛₗ[witt_vector.fraction_ring.frobenius_ring_hom p k] V

An isocrystal is a vector space over the field K(p, k) additionally equipped with a Frobenius-linear automorphism.

Instances of this typeclass

witt_vector.standard_one_dim_isocrystal.isocrystal

Instances of other typeclasses for witt_vector.isocrystal

witt_vector.isocrystal.has_sizeof_inst

def witt_vector.isocrystal.frobenius (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 ≃ₛₗ[witt_vector.fraction_ring.frobenius_ring_hom p k] V

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

Equations

witt_vector.isocrystal.frobenius p k = witt_vector.isocrystal.frob

@[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)

to_linear_map : V →ₗ[fraction_ring (witt_vector p k)] V₂
frob_equivariant : ∀ (x : V), ⇑(witt_vector.isocrystal.frobenius p k) (⇑(self.to_linear_map) x) = ⇑(self.to_linear_map) (⇑(witt_vector.isocrystal.frobenius p k) x)

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)

to_linear_equiv : V ≃ₗ[fraction_ring (witt_vector p k)] V₂
frob_equivariant : ∀ (x : V), ⇑(witt_vector.isocrystal.frobenius p k) (⇑(self.to_linear_equiv) x) = ⇑(self.to_linear_equiv) (⇑(witt_vector.isocrystal.frobenius p k) x)

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

module (fraction_ring (witt_vector p k)) (fraction_ring (witt_vector p k))

A helper instance for type class inference.

Equations

witt_vector.fraction_ring.module p k = semiring.to_module

@[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

witt_vector.standard_one_dim_isocrystal p k m = fraction_ring (witt_vector p k)

Instances for witt_vector.standard_one_dim_isocrystal

@[protected, instance]

noncomputable def witt_vector.standard_one_dim_isocrystal.add_comm_group (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] (m : ℤ) :

add_comm_group (witt_vector.standard_one_dim_isocrystal p k m)

@[protected, instance]

noncomputable def witt_vector.standard_one_dim_isocrystal.module (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] (m : ℤ) :

module (fraction_ring (witt_vector p k)) (witt_vector.standard_one_dim_isocrystal p k m)

@[protected, instance]

noncomputable def witt_vector.standard_one_dim_isocrystal.isocrystal (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] (m : ℤ) :

witt_vector.isocrystal p k (witt_vector.standard_one_dim_isocrystal p k m)

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

Equations

witt_vector.standard_one_dim_isocrystal.isocrystal p k m = {to_module := semiring.to_module ring.to_semiring, frob := (witt_vector.fraction_ring.frobenius p k).to_semilinear_equiv.trans (linear_equiv.smul_of_ne_zero (fraction_ring (witt_vector p k)) (fraction_ring (witt_vector p k)) (↑p ^ m) _)}

@[simp]

theorem witt_vector.standard_one_dim_isocrystal.frobenius_apply (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [comm_ring k] [is_domain k] [char_p k p] [perfect_ring k p] (m : ℤ) (x : witt_vector.standard_one_dim_isocrystal p k m) :

⇑(witt_vector.isocrystal.frobenius p k) x = ↑p ^ m • ⇑(witt_vector.fraction_ring.frobenius_ring_hom p k) x

theorem witt_vector.isocrystal_classification (p : ℕ) [fact (nat.prime p)] (k : Type u_1) [field k] [is_alg_closed k] [char_p k p] (V : Type u_2) [add_comm_group V] [witt_vector.isocrystal p k V] (h_dim : finite_dimensional.finrank (fraction_ring (witt_vector p k)) V = 1) :

∃ (m : ℤ), nonempty (witt_vector.isocrystal_equiv p k (witt_vector.standard_one_dim_isocrystal 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.