Commit 2024-04-16 10:25 d83efb31

refactor(CategoryTheory): more general form of the characterisation of condensed sets as sheaves on Stonean (#11518) Given a fully faithful functor F : C ⥤ D into a precoherent category, which preserves and reflects finite effective epi families, and satisfies the property F.EffectivelyEnough (meaning that to every object in C there is an effective epi from an object in the image of F), the categories of coherent sheaves on C and D are equivalent. We give the corresonding result for the regular topology as well. We use this general setup to refactor the characterisation of condensed sets as sheaves on Stonean; indeed, the inclusion functor to CompHaus satisfies Functor.EffectivelyEnough because the Stonean spaces are the projective objects in CompHaus, which has enough projectives and every epimorphism in CompHaus is effective.