Purity: upper shriek as a twist of pullback (Theorem 1.2.5 (i))

Disproved

RSF.purity

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

p-adic-geometrypuritysix-functor-formalism

Theorem 1.2.5 (i) of the thesis: for a bdcs and p-cohomologically smooth map f, the natural morphism from the tensor of the upper shriek of the structure sheaf with the pullback to the upper shriek functor is an isomorphism, and the upper shriek of the structure sheaf is invertible for the tensor product. Together with the proper special case of the formalism this is the input from which the trace map of Poincare duality is built.

Formalization Note The world is abstract interface data; the isomorphism is encoded as an equality of the bundled operations applied to objects.

Preamble

import Mathlib
import Definitions.Def_RSF_cat
import Definitions.Def_RSF_geo

Formal statement

namespace RSF

/-!  Theorem 1.2.5 (i) of the thesis: purity. For a bdcs and
p-cohomologically smooth map, upper shriek is the tensor product of the
upper shriek of the structure sheaf with the pullback, and the upper shriek
of the structure sheaf is invertible for the tensor product. Together with
the special case that lower shriek agrees with pushforward along proper
maps, this is the formal input from which Poincare duality follows.  -/

theorem purity : ∀ (w : SixFunctorWorld) (X Y : w.Space) (f : w.Map Y X),
    w.IsBdcs Y X f → w.IsPCohSmooth Y X f →
    (∀ M : w.C X,
      w.ushriek Y X f M = w.tensor Y (w.ushriek Y X f (w.unit X)) (w.pull Y X f M)) ∧
    IsInvertible w Y (w.ushriek Y X f (w.unit X)) := by
  sorry

end RSF

Source

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

Read-back

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

Restate: for every six-functor world, every map f from a space Y to a space X labeled bdcs and p-cohomologically smooth, and every object M of the category of X, the upper shriek of f at M equals the tensor of the upper shriek of f at the structure sheaf of X with the pullback of f at M; and the upper shriek of f at the structure sheaf of X is invertible - it has a two-sided inverse for the tensor product. No other hypotheses appear.

View graph