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

• Condensed.StoneanCompHaus.equivalence: the equivalence from coherent sheaves on Stonean to coherent sheaves on CompHaus (i.e. condensed sets).
• Condensed.StoneanProfinite.equivalence: the equivalence from coherent sheaves on Stonean to coherent sheaves on Profinite.
• Condensed.ProfiniteCompHaus.equivalence: the equivalence from coherent sheaves on Profinite to coherent sheaves on CompHaus (i.e. condensed sets).

noncomputable def Condensed.StoneanCompHaus.equivalence (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A ≌ Condensed A

The equivalence from coherent sheaves on Stonean to coherent sheaves on CompHaus (i.e. condensed sets).

Equations

• Condensed.StoneanCompHaus.equivalence A = CategoryTheory.coherentTopology.equivalence' Stonean.toCompHaus A

instance Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite : Stonean.toProfinite.PreservesEffectiveEpis

Equations

• Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite = ⋯

instance Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite : Stonean.toProfinite.ReflectsEffectiveEpis

Equations

• Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite = ⋯

noncomputable def Condensed.StoneanProfinite.stoneanToProfiniteEffectivePresentation (X : Profinite) : Stonean.toProfinite.EffectivePresentation X

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

Equations

• Condensed.StoneanProfinite.stoneanToProfiniteEffectivePresentation X = { p := X.presentation, f := Profinite.presentation.π X, effectiveEpi := ⋯ }

instance Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite : Stonean.toProfinite.EffectivelyEnough

Equations

• Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite = ⋯

noncomputable def Condensed.StoneanProfinite.equivalence (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : Profiniteᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toProfinite.op) A] : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A ≌ CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A

The equivalence from coherent sheaves on Stonean to coherent sheaves on Profinite.

Equations

• Condensed.StoneanProfinite.equivalence A = CategoryTheory.coherentTopology.equivalence' Stonean.toProfinite A

noncomputable def Condensed.ProfiniteCompHaus.equivalence (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A ≌ Condensed A

The equivalence from coherent sheaves on Profinite to coherent sheaves on CompHaus (i.e. condensed sets).

Equations

• Condensed.ProfiniteCompHaus.equivalence A = CategoryTheory.coherentTopology.equivalence' profiniteToCompHaus A

theorem Condensed.isSheafProfinite {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : Condensed A) [∀ (Y : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y profiniteToCompHaus.op) A] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) (profiniteToCompHaus.op.comp X.val)

theorem Condensed.isSheafStonean {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : Condensed A) [∀ (Y : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y Stonean.toCompHaus.op) A] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) (Stonean.toCompHaus.op.comp X.val)