Smooth maps are p-cohomologically smooth after diamondification (Theorem 1.2.6)

Disproved

RSF.smooth_p_cohomologically_smooth

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

diamondsp-adic-geometrysmoothness

Theorem 1.2.6 of the thesis: a smooth map of analytic adic spaces over Q_p induces, under the diamond functor, a p-cohomologically smooth map of diamonds. This is the bridge from the smoothness of classical rigid geometry to the p-cohomological smoothness in terms of which purity is stated; its proof reduces locally to Faltings' computation on the relative torus, through the smooth formal model and the Koszul complex of the perfectoid torus torsor.

Formalization Note The diamondification is an operation of the abstract world on maps, an idealization of the diamond functor; the adic smoothness label carries the arithmetic hypothesis of maps of analytic adic spaces over Q_p.

Preamble

import Mathlib
import Definitions.Def_RSF_cat
import Definitions.Def_RSF_geo

Formal statement

namespace RSF

/-!  Theorem 1.2.6 of the thesis: smooth maps of analytic adic spaces over
Q_p induce p-cohomologically smooth maps after diamondification. This is
the bridge from the smoothness of classical rigid geometry to the
p-cohomological smoothness in terms of which purity is stated, and it is
the step of the thesis whose proof reduces to Faltings' computation on the
relative torus.  -/

theorem smooth_p_cohomologically_smooth :
    ∀ (w : SixFunctorWorld) (X Y : w.Space) (f : w.Map X Y),
    w.IsAdicSmooth X Y f → w.IsPCohSmooth X Y (w.diamond X Y f) := by
  sorry

end RSF

Source

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

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 X to a space Y labeled adically smooth, the diamondification of f is labeled p-cohomologically smooth. No other hypotheses appear.

View graph