The explicit sheaf condition for condensed sets

We give the following three explicit descriptions of condensed sets:

• Condensed.ofSheafStonean: A finite-product-preserving presheaf on Stonean.

• Condensed.ofSheafProfinite: A finite-product-preserving presheaf on Profinite, satisfying EqualizerCondition.

• Condensed.ofSheafStonean: A finite-product-preserving presheaf on CompHaus, satisfying EqualizerCondition.

The property EqualizerCondition is defined in Mathlib/CategoryTheory/Sites/RegularExtensive.lean and it says that for any effective epi X ⟶ B (in this case that is equivalent to being a continuous surjection), the presheaf F exhibits F(B) as the equalizer of the two maps F(X) ⇉ F(X ×_B X)

theorem CategoryTheory.isSheaf_coherent_iff_regular_and_extensive {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ∧ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F

theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (F : CategoryTheory.Functor CompHausᵒᵖ (Type (u + 1))) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology CompHaus) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F) ∧ CategoryTheory.regularTopology.EqualizerCondition F

theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition' {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor CompHausᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology CompHaus) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)) ∧ CategoryTheory.regularTopology.EqualizerCondition (F.comp G)

theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F) ∧ CategoryTheory.regularTopology.EqualizerCondition F

theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition' {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor Profiniteᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)) ∧ CategoryTheory.regularTopology.EqualizerCondition (F.comp G)

theorem Stonean.isSheaf_iff_preservesFiniteProducts (F : CategoryTheory.Functor Stoneanᵒᵖ (Type (u + 1))) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)

theorem Stonean.isSheaf_iff_preservesFiniteProducts' {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor Stoneanᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (F.comp G))

noncomputable def Condensed.ofSheafStonean {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor Stoneanᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] : Condensed A

The condensed set associated to a finite-product-preserving presheaf on Stonean.

Equations

• Condensed.ofSheafStonean G F = (Condensed.StoneanCompHaus.equivalence A).functor.obj { val := F, cond := ⋯ }

noncomputable def Condensed.ofSheafProfinite {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor Profiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp G)) : Condensed A

The condensed set associated to a presheaf on Profinite which preserves finite products and satisfies the equalizer condition.

Equations

• Condensed.ofSheafProfinite G F hF = (Condensed.ProfiniteCompHaus.equivalence A).functor.obj { val := F, cond := ⋯ }

noncomputable def Condensed.ofSheafCompHaus {A : Type (u + 2)} [CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1))) [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits G] [G.ReflectsIsomorphisms] (F : CategoryTheory.Functor CompHausᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp G)) : Condensed A

The condensed set associated to a presheaf on CompHaus which preserves finite products and satisfies the equalizer condition.

Equations

• Condensed.ofSheafCompHaus G F hF = { val := F, cond := ⋯ }

@[reducible, inline]

noncomputable abbrev CondensedSet.ofSheafStonean (F : CategoryTheory.Functor Stoneanᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] : CondensedSet

A CondensedSet version of Condensed.ofSheafStonean. 

Equations

• CondensedSet.ofSheafStonean F = Condensed.ofSheafStonean (CategoryTheory.Functor.id (Type (u + 1))) F

@[reducible, inline]

noncomputable abbrev CondensedSet.ofSheafProfinite (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : CondensedSet

A CondensedSet version of Condensed.ofSheafProfinite. 

Equations

• CondensedSet.ofSheafProfinite F hF = Condensed.ofSheafProfinite (CategoryTheory.Functor.id (Type (u + 1))) F hF

@[reducible, inline]

noncomputable abbrev CondensedSet.ofSheafCompHaus (F : CategoryTheory.Functor CompHausᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : CondensedSet

A CondensedSet version of Condensed.ofSheafCompHaus. 

Equations

• CondensedSet.ofSheafCompHaus F hF = Condensed.ofSheafCompHaus (CategoryTheory.Functor.id (Type (u + 1))) F hF

theorem CondensedSet.equalizerCondition (X : CondensedSet) : CategoryTheory.regularTopology.EqualizerCondition X.val

A condensed set satisfies the equalizer condition.

noncomputable instance CondensedSet.instPreservesFiniteProductsOppositeCompHausVal (X : CondensedSet) : CategoryTheory.Limits.PreservesFiniteProducts X.val

A condensed set preserves finite products.

Equations

• X.instPreservesFiniteProductsOppositeCompHausVal = ⋯.some

noncomputable instance CondensedSet.instPreservesFiniteProductsOppositeProfiniteVal (Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) (Type (u + 1))) : CategoryTheory.Limits.PreservesFiniteProducts Y.val

A condensed set regarded as a sheaf on Profinite preserves finite products.

Equations

• CondensedSet.instPreservesFiniteProductsOppositeProfiniteVal Y = ⋯.some

noncomputable instance CondensedSet.instPreservesFiniteProductsOppositeStoneanVal (Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) (Type (u + 1))) : CategoryTheory.Limits.PreservesFiniteProducts Y.val

A condensed set regarded as a sheaf on Stonean preserves finite products.

Equations

• CondensedSet.instPreservesFiniteProductsOppositeStoneanVal Y = ⋯.some

@[reducible, inline]

noncomputable abbrev CondensedMod.ofSheafStonean (R : Type (u + 1)) [Ring R] (F : CategoryTheory.Functor Stoneanᵒᵖ (ModuleCat R)) [CategoryTheory.Limits.PreservesFiniteProducts F] : CondensedMod R

A CondensedMod version of Condensed.ofSheafStonean. 

Equations

• CondensedMod.ofSheafStonean R F = Condensed.ofSheafStonean (CategoryTheory.forget (ModuleCat R)) F

@[reducible, inline]

noncomputable abbrev CondensedMod.ofSheafProfinite (R : Type (u + 1)) [Ring R] (F : CategoryTheory.Functor Profiniteᵒᵖ (ModuleCat R)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget (ModuleCat R)))) : CondensedMod R

A CondensedMod version of Condensed.ofSheafProfinite. 

Equations

• CondensedMod.ofSheafProfinite R F hF = Condensed.ofSheafProfinite (CategoryTheory.forget (ModuleCat R)) F hF

@[reducible, inline]

noncomputable abbrev CondensedMod.ofSheafCompHaus (R : Type (u + 1)) [Ring R] (F : CategoryTheory.Functor CompHausᵒᵖ (ModuleCat R)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget (ModuleCat R)))) : CondensedMod R

A CondensedMod version of Condensed.ofSheafCompHaus. 

Equations

• CondensedMod.ofSheafCompHaus R F hF = Condensed.ofSheafCompHaus (CategoryTheory.forget (ModuleCat R)) F hF