The pro-\'etale topology for schemes

We give a new definition of the derived category of constructible $\mathrm{\ell }$-adic sheaves on a scheme, which is as simple as the geometric intuition behind them. Moreover, we define a refined fundamental group of schemes, which is large enough to see all lisse $\mathrm{\ell }$-adic sheaves, even on non-normal schemes. To accomplish these tasks, we define and study the pro-'etale topology, which is a Grothendieck topology on schemes that is closely related to the 'etale topology, and yet better suited for infinite constructions typically encountered in $\mathrm{\ell }$-adic cohomology. An essential foundational result is that this site is locally contractible in a well-defined sense.