The explicit sheaf condition for condensed sets

We give the following three explicit descriptions of condensed objects:

• 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/RegularSheaves.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)

We also give variants for condensed objects in concrete categories whose forgetful functor reflects finite limits (resp. products), where it is enough to check the sheaf condition after postcomposing with the forgetful functor.

noncomputable def Condensed.ofSheafStonean {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] (F : CategoryTheory.Functor Stoneanᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] : Condensed A

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

Equations

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

noncomputable def Condensed.ofSheafForgetStonean {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.Limits.ReflectsFiniteProducts (CategoryTheory.forget A)] (F : CategoryTheory.Functor Stoneanᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] : Condensed A

The condensed object associated to a presheaf on Stonean whose postcomposition with the forgetful functor preserves finite products.

Equations

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

noncomputable def Condensed.ofSheafProfinite {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] (F : CategoryTheory.Functor Profiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : Condensed A

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

Equations

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

noncomputable def Condensed.ofSheafForgetProfinite {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] (F : CategoryTheory.Functor Profiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A))) : Condensed A

The condensed object associated to a presheaf on Profinite whose postcomposition with the forgetful functor preserves finite products and satisfies the equalizer condition.

Equations

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

noncomputable def Condensed.ofSheafCompHaus {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (F : CategoryTheory.Functor CompHausᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : Condensed A

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

Equations

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

noncomputable def Condensed.ofSheafForgetCompHaus {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] (F : CategoryTheory.Functor CompHausᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A))) : Condensed A

The condensed object associated to a presheaf on CompHaus whose postcomposition with the forgetful functor preserves finite products and satisfies the equalizer condition.

Equations

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

theorem Condensed.equalizerCondition {A : Type u_1} [CategoryTheory.Category.{u_3, u_1} A] (X : Condensed A) : CategoryTheory.regularTopology.EqualizerCondition X.val

A condensed object satisfies the equalizer condition.

noncomputable instance Condensed.instPreservesFiniteProductsOppositeCompHausVal {A : Type u_1} [CategoryTheory.Category.{u_3, u_1} A] (X : Condensed A) : CategoryTheory.Limits.PreservesFiniteProducts X.val

A condensed object preserves finite products.

Equations

• ⋯ = ⋯

noncomputable instance Condensed.instPreservesFiniteProductsOppositeProfiniteVal {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A) : CategoryTheory.Limits.PreservesFiniteProducts X.val

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

Equations

• ⋯ = ⋯

theorem Condensed.equalizerCondition_profinite {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A) : CategoryTheory.regularTopology.EqualizerCondition X.val

A condensed object regarded as a sheaf on Profinite satisfies the equalizer condition.

noncomputable instance Condensed.instPreservesFiniteProductsOppositeStoneanVal {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A) : CategoryTheory.Limits.PreservesFiniteProducts X.val

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

Equations

• ⋯ = ⋯

@[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 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 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 F hF

@[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 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) : CondensedMod R

A CondensedMod version of Condensed.ofSheafProfinite.

Equations

• CondensedMod.ofSheafProfinite R F hF = Condensed.ofSheafProfinite 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) : CondensedMod R

A CondensedMod version of Condensed.ofSheafCompHaus.

Equations

• CondensedMod.ofSheafCompHaus R F hF = Condensed.ofSheafCompHaus F hF