# 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

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.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : ) :
(∃ (α : Type) (x : ) (Y : αStonean) (π : (a : α) → Y a X), ∀ (a : α), S.arrows (π a))
Equations
• One or more equations did not get rendered due to their size.
noncomputable def Condensed.StoneanCompHaus.equivalence (A : Type u_1) [] :

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.
Instances For
theorem Condensed.StoneanProfinite.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : ) :
(∃ (α : Type) (x : ) (Y : αStonean) (π : (a : α) → Y a X), ∀ (a : α), S.arrows (π a))
Equations
• One or more equations did not get rendered due to their size.
noncomputable def Condensed.StoneanProfinite.equivalence (A : Type u_1) [] :

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.
Instances For
noncomputable def Condensed.ProfiniteCompHaus.equivalence (A : Type u_1) [] :

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

Equations
Instances For