Theorems · Theorem · number theory

WittVector.isocrystal_classification

∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_2) [inst_1 : Field k] [inst_2 : IsAlgClosed k] [inst_3 : CharP k p]
  (V : Type u_3) [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V],
  Module.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.

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

0 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactFieldIsAlgClosedCharPAddCommGroupWittVector.Isocrystal