Proétale cohomology in Lean

This repository contains a (WIP) formalisation of (pro)étale cohomology in Lean following the paper [BS13] by Bhatt and Scholze.

A long-term goal of this project is to formalise Theorem 5.6.2 in [BS13], which implies the following theorem: Let be a variety over an algebraically closed field . Let be a prime different from the characteristic of . One has , where the RHS is interpreted naively as cohomology of the proétale site of , the LHS is defined as the inverse limit