Poincare duality for F_p-cohomology (Corollary 1.2.9, the goal)
DisprovedRSF.poincare_duality_pCorollary 1.2.9 of the thesis, the case l = p of Theorem 1.1.1 and the goal of this mission: if K is a non-archimedean field over Q_p and X is a proper smooth rigid-analytic space of pure dimension d over K, then for every integer i there is a natural perfect pairing between H^i(X_et, F_p) and H^(2d-i)(X_et, F_p) with values in the Tate object F_p(-d). The thesis deduces it from the six-functor formalism: lower shriek agrees with pushforward along the proper structure map; the twist computation identifies the upper shriek of the structure sheaf with the Tate twist shifted by the dimension; the p-torsion Riemann-Hilbert correspondence transports the result to etale F_p-sheaves; and the trace pairing obtained from the resulting adjunction is perfect. The deduction is the proposed work of the goal.
Formalization Note The base field, the variety, and the cohomology groups are abstract interface data carrying the geometric conditions as labels; the perfectness of the pairing is encoded as bilinearity in both arguments, nondegeneracy in both arguments, and exhaustiveness against the bundled linear functionals.
import Mathlib import Definitions.Def_RSF_cat import Definitions.Def_RSF_geo
namespace RSF
/-! The goal: Corollary 1.2.9 of the thesis, Poincare duality for the etale
F_p-cohomology of a proper smooth rigid-analytic variety - the case ell = p
of Theorem 1.1.1, which the thesis proves through the six-functor
formalism, the p-cohomological smoothness of smooth maps, the p-torsion
Riemann-Hilbert correspondence, and the twist computation. On a proper
smooth rigid-analytic variety of pure dimension d over a non-archimedean
field of mixed characteristic (0, p), the etale cohomology with
coefficients in F_p admits, in every degree, a pairing against the
complementary degree with values in the Tate object F_p(-d) which is
bilinear in both arguments, nondegenerate in both arguments, and
exhaustive - a perfect pairing. The deduction from the milestones is the
proposed work of the mission. -/
theorem poincare_duality_p : ∀ w : RigidCohWorld,
w.ℓ = w.P →
w.nonarchField → w.algClosed → w.mixedChar →
w.properSmooth → w.pureDim →
∃ pair : ∀ i : ℤ, w.H (2 * (w.d : ℤ) - i) → w.H i → w.Tate,
(∀ (i : ℤ) (x y : w.H (2 * (w.d : ℤ) - i)) (z : w.H i),
pair i (w.add (2 * (w.d : ℤ) - i) x y) z = w.tadd (pair i x z) (pair i y z)) ∧
(∀ (i : ℤ) (k : ZMod w.ℓ) (x : w.H (2 * (w.d : ℤ) - i)) (z : w.H i),
pair i (w.smul (2 * (w.d : ℤ) - i) k x) z = w.tsmul k (pair i x z)) ∧
(∀ (i : ℤ) (x : w.H (2 * (w.d : ℤ) - i)) (y z : w.H i),
pair i x (w.add i y z) = w.tadd (pair i x y) (pair i x z)) ∧
(∀ (i : ℤ) (k : ZMod w.ℓ) (x : w.H (2 * (w.d : ℤ) - i)) (z : w.H i),
pair i x (w.smul i k z) = w.tsmul k (pair i x z)) ∧
(∀ (i : ℤ) (x : w.H (2 * (w.d : ℤ) - i)),
(∀ z : w.H i, pair i x z = w.tzero) → x = w.zero (2 * (w.d : ℤ) - i)) ∧
(∀ (i : ℤ) (z : w.H i),
(∀ x : w.H (2 * (w.d : ℤ) - i), pair i x z = w.tzero) → z = w.zero i) ∧
(∀ (i : ℤ) (φ : ZModLinear w.ℓ (w.H i) w.Tate
(w.add i) (w.zero i) (w.smul i) w.tadd w.tzero w.tsmul),
∃ u : w.H (2 * (w.d : ℤ) - i), ∀ z : w.H i, pair i u z = φ.map z) := by
sorry
end RSF
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every rigid cohomology world whose prime l equals its residue characteristic p and whose labels assert that the base field is a non-archimedean algebraically closed field of mixed characteristic and that the variety is proper, smooth, of pure dimension d, there is a family of pairings, one per integer degree i, from the cohomology group in degree 2d - i against the cohomology group in degree i, with values in the Tate object, which is additive and ZMod-p-equivariant in both arguments, nondegenerate in both arguments against the respective zeros, and exhaustive: every bundled ZMod-p-linear functional on the degree i group is the pairing against some vector of the degree 2d - i group. This is the goal statement of the mission.