Pro-étale cohomology

Blueprint Summary🔗

Overview
Total entries249completed: 116; deps incomplete: 31; sorries: 27; no proof: 54
Ready now27Entries whose next formalization step is currently unblocked.
Fully closed116Local code and prerequisite closure are both complete.
Actionable priorities56Entries ready now and already unlocking downstream work.
Current blockers33Missing external or incomplete Lean declarations.
Missing informal coverage26Entries with Lean code but missing an informal statement or proof block.
Ready next (56)
Current blockers (33)
Missing informal coverage (26)
Entry index (249)
Definitions54completed: 28; deps incomplete: 5; sorries: 0; no proof: 0
Propositions26completed: 2; deps incomplete: 5; sorries: 1; no proof: 18
Lemmas146completed: 83; deps incomplete: 15; sorries: 22; no proof: 26
Theorems9completed: 2; deps incomplete: 2; sorries: 3; no proof: 2
Corollaries14completed: 1; deps incomplete: 4; sorries: 1; no proof: 8
Informal-only entries75
Definition Index (54)
Theorem / Proposition / Lemma / Corollary Index (195)
By parent groups (5)
Pro-categories, precoherent categories, the coherent topology and generated topologies, used to compare sites with their pro-completions. (14)
Replete categories, coherent objects, and weakly contractible objects, following Section 3 of Bhatt–Scholze. (6)
The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (27)
Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (105)
Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project. (43)
Dependency insights
Statement-used entries68Entries reused in statement dependencies.
Proof-used entries164Entries reused in proof-only dependencies.
Tracked parent groups5Grouped health rollups for parents with more than one child entry.
Most used in statements (68)
Most used in proofs (164)
Group health (5)
  • Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project.«more-on-local-structure»
    Grouped view over entries sharing the same parent.
    total: 46closed: 20local-only: 2ready: 24blocked: 0incomplete Lean: 17unlock score: 691
    Next: «lem:local-dim-zero-tensor» stage: proofdownstream unlocks: 17
  • Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project.«local-structure»
    Grouped view over entries sharing the same parent.
    total: 137closed: 89local-only: 16ready: 18blocked: 14incomplete Lean: 9unlock score: 1754
    Next: «def:p-henselian» stage: statementdownstream unlocks: 29
  • Pro-categories, precoherent categories, the coherent topology and generated topologies, used to compare sites with their pro-completions.«pro-categories»
    Grouped view over entries sharing the same parent.
    total: 17closed: 0local-only: 4ready: 11blocked: 2incomplete Lean: 0unlock score: 61
    Next: «prop:pro-univ-prop» stage: proofdownstream unlocks: 13
  • The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze.«proetale-topology»
    Grouped view over entries sharing the same parent.
    total: 37closed: 3local-only: 9ready: 9blocked: 16incomplete Lean: 1unlock score: 229
    Next: «def:small-P-site» stage: statementdownstream unlocks: 20
  • Replete categories, coherent objects, and weakly contractible objects, following Section 3 of Bhatt–Scholze.replete
    Grouped view over entries sharing the same parent.
    total: 12closed: 4local-only: 0ready: 4blocked: 4incomplete Lean: 0unlock score: 29
    Next: «lemma:replete-lim-lim-epi» stage: proofdownstream unlocks: 3
Metadata
Tags in use1Distinct tags currently attached to blueprint entries.
Tag rollups (1)
  • tag: mathlib
    entries: 22actionable: 6quick wins: 0linked PRs: 0
Metadata audit
Missing owner249
Missing effort249
Untagged227
Missing owner (249)
Missing effort (249)
Untagged (227)
Structure and coverage
Informal-only75Statements with no associated Lean code yet.
Ready to formalize27Entries whose next step is currently unblocked.
Formalized, ancestors open31Local Lean work is done, but prerequisite closure is still open.
Fully closed116Local code and ancestor closure are both complete.
Heaviest prerequisites (171)
No prerequisites (78)
No dependents (27)
Proof debt hotspots (3)
  • Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project.«more-on-local-structure»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 17incomplete decls: 19missing decls: 0total debt: 19
  • Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project.«local-structure»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 9incomplete decls: 13missing decls: 0total debt: 13
  • The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze.«proetale-topology»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1