Documentation

Mathlib.Condensed.Equivalence

Sheaves on CompHaus are equivalent to sheaves on Stonean #

The forgetful functor from extremally disconnected spaces Stonean to compact Hausdorff spaces CompHaus has the marvellous property that it induces an equivalence of categories between sheaves on these two sites. With the terminology of nLab, Stonean is a dense subsite of CompHaus: see https://ncatlab.org/nlab/show/dense+sub-site

Since Stonean spaces are the projective objects in CompHaus, which has enough projectives, and the notions of effective epimorphism, epimorphism and surjective continuous map are equivalent in CompHaus and Stonean, we can use the general setup in Mathlib.CategoryTheory.Sites.Coherent.SheafComparison to deduce the equivalence of categories. We give the corresponding statements for Profinite as well.

Main results #

An effective presentation of an X : Profinite with respect to the inclusion functor from Stonean

Equations
Instances For