The primitive comparison theorem (Scholze, cited as [34, Theorem 5.1])

Disproved

RSF.primitive_comparison

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

comparison-theoremetale-cohomologyrigid-analytic-geometry

The primitive comparison theorem cited by the thesis as [34, Theorem 5.1], due to Scholze: on a proper smooth rigid-analytic variety, the etale cohomology of the integral structure sheaves O^+/pi computes the etale cohomology with coefficients in F_p - the two cohomology theories are isomorphic degree by degree, compatibly with the addition and the zero. This is the comparison anchor on the way from the O^+/pi-sheaves of the six-functor formalism to the F_p-cohomology of the goal.

Formalization Note The two cohomology families and the proper smooth label are abstract interface data; constructing them for the actual cohomology theories is part of the proposed work.

Preamble

import Mathlib
import Definitions.Def_RSF_cat
import Definitions.Def_RSF_geo

Formal statement

namespace RSF

/-!  The primitive comparison theorem of Scholze, cited as [34, Theorem 5.1]
by the thesis: on a proper smooth rigid-analytic variety, the etale
cohomology of the structure sheaves O^+/pi computes the etale cohomology
with coefficients in F_p - the two cohomology theories are isomorphic
degree by degree, compatibly with the bundled addition and zero. This is
the comparison anchor on the way from the O^+/pi-sheaves of the six-functor
formalism to the F_p-cohomology of the goal.  -/

theorem primitive_comparison : ∀ w : ComparisonWorld,
    w.properSmooth →
    ∃ e : ∀ i : ℤ, w.A i ≃ w.B i,
      (∀ (i : ℤ) (x y : w.A i),
        e i (w.aadd i x y) = w.badd i (e i x) (e i y)) ∧
      (∀ i : ℤ, e i (w.azero i) = w.bzero i) := by
  sorry

end RSF

Source

L. Mann, A p-Adic 6-Functor Formalism in Rigid-Analytic Geometry, arXiv:2206.02022 (2022), page 4 (the Primitive Comparison Theorem cited as [34, Theorem 5.1]); P. Scholze, p-adic Hodge theory for rigid-analytic varieties, Forum of Mathematics Pi 1 (2013), Theorem 5.1.

Read-back

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

Restate: for every comparison world whose label asserts proper smoothness, there is a family of bijections, one per integer degree, from the first cohomology family to the second, which respects the bundled additions and maps the bundled zeros to the bundled zeros. No other hypotheses appear.

View graph