instIsocrystalStandardOneDimIsocrystal

English

The standard one-dimensional isocrystal is instantiated for slope m as an isocrystal object.

Русский

Стандартная одномерная изокристалл создаётся как объект изокристалла со slope m.

LaTeX

$$$\text{instIsocrystalStandardOneDimIsocrystal}(p) (m) : \text{Isocrystal}(p,k, S(p,k,m))$$$

Lean4

/-- The standard one-dimensional isocrystal of slope `m : ℤ` is an isocrystal. -/
instance (m : ℤ) : Isocrystal p k (StandardOneDimIsocrystal p k m) where
  frob :=
    (FractionRing.frobenius p k).toSemilinearEquiv.trans
      (LinearEquiv.smulOfNeZero _ _ _ (zpow_ne_zero m (WittVector.FractionRing.p_nonzero p k)))

Похожие утверждения