Pro-étale cohomology

 Pro-étale cohomology🔗

Compiled2026-07-14T09:59:10ZProjectc815a07feat: update comparator files (#193)Leanleanprover/lean4:v4.30.0VersoBlueprintv4.30.0@11c82ed5b844Mathlib9a568f0b75d28670664e6d6862d6e01c4625e380@9a568f0b75d2

This blueprint tracks the formalisation of (pro)étale cohomology in Lean, following the paper The pro-étale topology for schemes by Bhatt and Scholze. A long-term goal of the project is Theorem 5.6.2 of that paper, comparing étale and pro-étale cohomology with \overline{\mathbb{Q}}_\ell-coefficients for varieties over an algebraically closed field.

Contents

  1. 1. Local structures
  2. 2. More on local structure
  3. 3. Replete categories
  4. 4. Pro-categories
  5. 5. The pro-étale topology
  6. Dependency Graph
  7. Blueprint Summary