A p-torsion Riemann-Hilbert correspondence (Theorem 1.2.7)

Disproved

RSF.riemann_hilbert

by Lucas · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

frobeniusp-adic-hodge-theoryriemann-hilbert

Theorem 1.2.7 of the thesis: on a small v-stack over Z_p with pseudouniformizer pi dividing p, the functor of tensoring an overconvergent etale F_p-sheaf with the structure sheaves O^+a/pi, which lands in phi-modules - modules with a Frobenius-semilinear structure whose Frobenius pullback is invertible - is fully faithful, and it induces an equivalence of the perfect objects on both sides: every perfect phi-module is the image of an etale sheaf, and the image of an etale sheaf is perfect. This correspondence carries the almost purity information that links the O^+/pi-cohomology of the six-functor formalism to the F_p-cohomology of the goal.

Formalization Note The Riemann-Hilbert world is abstract interface data; full faithfulness is the bijectivity of the action on hom-types, and the equivalence on perfect objects is encoded through the object-level image and the perfectness predicate.

Preamble

import Mathlib
import Definitions.Def_RSF_cat
import Definitions.Def_RSF_geo

Formal statement

namespace RSF

/-!  Theorem 1.2.7 of the thesis: a p-torsion Riemann-Hilbert correspondence.
The functor of tensoring an overconvergent etale F_p-sheaf with the
structure sheaves O^+a/pi, landing in phi-modules, is fully faithful, and
it induces an equivalence of the perfect objects on both sides: every
perfect phi-module is the image of an etale sheaf, and the image of an
etale sheaf is perfect. This correspondence carries the information of
Faltings' almost purity that links the O^+/pi-cohomology of the six-functor
formalism to the F_p-cohomology of the goal.  -/

theorem riemann_hilbert : ∀ w : RHWorld,
    (∀ A B : w.Sheaf, Function.Bijective (w.Tmor A B)) ∧
    (∀ M : w.PhiMod, w.IsPerfect M → ∃ N : w.Sheaf, w.T N = M) ∧
    (∀ N : w.Sheaf, w.IsPerfect (w.T N)) := by
  sorry

end RSF

Source

L. Mann, A p-Adic 6-Functor Formalism in Rigid-Analytic Geometry, arXiv:2206.02022 (2022), Theorem 1.2.7 (proved as Theorem 3.9.23).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: for every Riemann-Hilbert world, the functor's action on hom-types is bijective for every pair of sheaves; every phi-module labeled perfect is the image of some sheaf under the functor; and the image of every sheaf is labeled perfect. No other hypotheses appear.

View graph