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

Mathlib has isolated three properties called CoverDense, CoverPreserving and CoverLifting, which between them imply that Stonean is a dense subsite, and it also has the construction of the equivalence of the categories of sheaves, given these three properties.

Main theorems

• Condensed.StoneanCompHaus.isCoverDense, Condensed.StoneanCompHaus.coverPreserving, Condensed.StoneanCompHaus.coverLifting: the three conditions needed to guarantee the equivalence of the categories of sheaves on the coherent site on Stonean on the one hand and CompHaus on the other.
• Condensed.StoneanProfinite.coverDense, Condensed.StoneanProfinite.coverPreserving, Condensed.StoneanProfinite.coverLifting: the corresponding conditions comparing the coherent sites on Stonean and Profinite.
• 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).

theorem Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology (B : CompHaus) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton (CompHaus.presentation.π B)) ∈ (CategoryTheory.coherentTopology CompHaus).sieves B

instance Condensed.StoneanCompHaus.isCoverDense : CategoryTheory.Functor.IsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)

Equations

• Condensed.StoneanCompHaus.isCoverDense = (_ : CategoryTheory.Functor.IsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus))

theorem Condensed.StoneanCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : CategoryTheory.Sieve X) : (∃ (α : Type) (x : Fintype α) (Y : α → Stonean) (π : (a : α) → Y a ⟶ X), CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔ S ∈ (CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)).sieves X

theorem Condensed.StoneanCompHaus.coherentTopology_is_induced : CategoryTheory.coherentTopology Stonean = CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)

theorem Condensed.StoneanCompHaus.coverPreserving : CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology CompHaus) Stonean.toCompHaus

instance Condensed.StoneanCompHaus.coverLifting : CategoryTheory.Functor.IsCocontinuous Stonean.toCompHaus (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology CompHaus)

Equations

• One or more equations did not get rendered due to their size.

instance Condensed.StoneanCompHaus.instIsContinuousStoneanInstLargeCategoryStoneanCompHausCategoryToCompHausCoherentTopologyInstPrecoherentToFinitaryPreExtensiveInstFinitaryExtensiveStoneanInstLargeCategoryStoneanInstPreregularStoneanInstLargeCategoryStoneanInstFinitaryExtensiveCompHausCategoryInstPreregularCompHausCategory : CategoryTheory.Functor.IsContinuous Stonean.toCompHaus (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology CompHaus)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Condensed.StoneanCompHaus.equivalence (A : Type u_1) [CategoryTheory.Category.{u + 1, u_1} A] [CategoryTheory.Limits.HasLimits 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

• One or more equations did not get rendered due to their size.

theorem Condensed.StoneanProfinite.generate_singleton_mem_coherentTopology (B : Profinite) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton (Profinite.presentation.π B)) ∈ (CategoryTheory.coherentTopology Profinite).sieves B

instance Condensed.StoneanProfinite.coverDense : CategoryTheory.Functor.IsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)

Equations

• Condensed.StoneanProfinite.coverDense = (_ : CategoryTheory.Functor.IsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite))

theorem Condensed.StoneanProfinite.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : CategoryTheory.Sieve X) : (∃ (α : Type) (x : Fintype α) (Y : α → Stonean) (π : (a : α) → Y a ⟶ X), CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔ S ∈ (CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)).sieves X

theorem Condensed.StoneanProfinite.coherentTopology_is_induced : CategoryTheory.coherentTopology Stonean = CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)

theorem Condensed.StoneanProfinite.coverPreserving : CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology Profinite) Stonean.toProfinite

instance Condensed.StoneanProfinite.isCocontinuous : CategoryTheory.Functor.IsCocontinuous Stonean.toProfinite (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology Profinite)

Equations

• One or more equations did not get rendered due to their size.

instance Condensed.StoneanProfinite.instIsContinuousStoneanInstLargeCategoryStoneanProfiniteCategoryToProfiniteCoherentTopologyInstPrecoherentToFinitaryPreExtensiveInstFinitaryExtensiveStoneanInstLargeCategoryStoneanInstPreregularStoneanInstLargeCategoryStoneanInstFinitaryExtensiveProfiniteCategoryInstPreregularProfiniteCategory : CategoryTheory.Functor.IsContinuous Stonean.toProfinite (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology Profinite)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Condensed.StoneanProfinite.equivalence (A : Type u_1) [CategoryTheory.Category.{u + 1, u_1} A] [CategoryTheory.Limits.HasLimits 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

• One or more equations did not get rendered due to their size.

noncomputable def Condensed.ProfiniteCompHaus.equivalence (A : Type u_1) [CategoryTheory.Category.{u + 1, u_1} A] [CategoryTheory.Limits.HasLimits 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 = (Condensed.StoneanProfinite.equivalence A).symm.trans (Condensed.StoneanCompHaus.equivalence A)