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 #

source
theorem Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology (B : CompHaus) :
CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton (CompHaus.presentation.π B)) ∈ (CategoryTheory.coherentTopology CompHaus).sieves B
source
instance Condensed.StoneanCompHaus.isCoverDense :
CategoryTheory.Functor.IsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)
Equations
source
theorem Condensed.StoneanCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : CategoryTheory.Sieve X) :
(∃ (α : Type) (_ : Finite α) (Y : α → Stonean) (π : (a : α) → Y a ⟶ X), CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔ S ∈ (CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)).sieves X
source
theorem Condensed.StoneanCompHaus.coherentTopology_is_induced :
CategoryTheory.coherentTopology Stonean = CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toCompHaus (CategoryTheory.coherentTopology CompHaus)
source
theorem Condensed.StoneanCompHaus.coverPreserving :
CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology CompHaus) Stonean.toCompHaus
source
instance Condensed.StoneanCompHaus.coverLifting :
CategoryTheory.Functor.IsCocontinuous Stonean.toCompHaus (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology CompHaus)
Equations
source
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.
source
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.
Instances For
    source
    theorem Condensed.StoneanProfinite.generate_singleton_mem_coherentTopology (B : Profinite) :
    CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton (Profinite.presentation.π B)) ∈ (CategoryTheory.coherentTopology Profinite).sieves B
    source
    instance Condensed.StoneanProfinite.coverDense :
    CategoryTheory.Functor.IsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)
    Equations
    source
    theorem Condensed.StoneanProfinite.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : CategoryTheory.Sieve X) :
    (∃ (α : Type) (_ : Finite α) (Y : α → Stonean) (π : (a : α) → Y a ⟶ X), CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔ S ∈ (CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)).sieves X
    source
    theorem Condensed.StoneanProfinite.coherentTopology_is_induced :
    CategoryTheory.coherentTopology Stonean = CategoryTheory.Functor.inducedTopologyOfIsCoverDense Stonean.toProfinite (CategoryTheory.coherentTopology Profinite)
    source
    theorem Condensed.StoneanProfinite.coverPreserving :
    CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology Profinite) Stonean.toProfinite
    source
    instance Condensed.StoneanProfinite.isCocontinuous :
    CategoryTheory.Functor.IsCocontinuous Stonean.toProfinite (CategoryTheory.coherentTopology Stonean) (CategoryTheory.coherentTopology Profinite)
    Equations
    source
    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.
    source
    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.
    Instances For
      source
      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
      Instances For