The upper shriek of the structure sheaf along a smooth map (Theorem 1.2.8)

Disproved

RSF.twist_computation

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

p-adic-geometrypuritytate-twist

Theorem 1.2.8 of the thesis: for a smooth map f of analytic adic spaces over Q_p of pure dimension d, the upper shriek of the structure sheaf is the structure sheaf of the source, Tate twisted by d and shifted by 2d: f^!(O_X^+a/p) = O_Y^+a/p(d)[2d]. The proof passes through the p-cohomological smoothness of the diamondified map, purity, and the Riemann-Hilbert correspondence, and identifies the relative dualizing sheaf up to which Poincare duality is stated.

Formalization Note The shift and the Tate twist are bundled operations of the abstract world; the isomorphism is encoded as an equality of objects.

Preamble

import Mathlib
import Definitions.Def_RSF_cat
import Definitions.Def_RSF_geo

Formal statement

namespace RSF

/-!  Theorem 1.2.8 of the thesis: the computation of the upper shriek of the
structure sheaf along a smooth map of pure dimension d: it is the structure
sheaf of the source, Tate twisted by d and shifted by 2d. Together with
purity this identifies the relative dualizing sheaf, and with the proper
special case of Theorem 1.2.4 it produces the trace map whose perfectness
is Poincare duality.  -/

theorem twist_computation :
    ∀ (w : SixFunctorWorld) (X Y : w.Space) (f : w.Map Y X) (d : ℕ),
    w.IsAdicSmooth Y X f → w.IsPureDim Y X f d →
    w.ushriek Y X f (w.unit X) = w.shift Y (2 * d) (w.tateTwist Y d (w.unit Y)) := by
  sorry

end RSF

Source

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

Read-back

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

Restate: for every six-functor world and every map f from a space Y to a space X labeled adically smooth and of pure dimension d, the upper shriek of f at the structure sheaf of X equals the shift by 2d of the Tate twist by d of the structure sheaf of Y. No other hypotheses appear.

View graph