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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C)) F ∧ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C)) F

theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (F : CategoryTheory.Functor CompHausᵒᵖ (Type (u + 1))) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology CompHaus) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F) ∧ CategoryTheory.regularCoverage.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] [CategoryTheory.ReflectsIsomorphisms G] (F : CategoryTheory.Functor CompHausᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology CompHaus) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Functor.comp F G)) ∧ CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F G)

noncomputable instance CompHaus.instPreservesFiniteProductsTypeTypesCompObjOppositeToQuiverToCategoryStructOppositeFunctorToQuiverToCategoryStructCategoryToPrefunctorCoyonedaOp {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor B A) (E : A) [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Functor.comp F (CategoryTheory.coyoneda.obj (Opposite.op E)))

Equations

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

theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology Profinite) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F) ∧ CategoryTheory.regularCoverage.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] [CategoryTheory.ReflectsIsomorphisms G] (F : CategoryTheory.Functor Profiniteᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Functor.comp F G)) ∧ CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F G)

theorem Stonean.isSheaf_iff_preservesFiniteProducts (F : CategoryTheory.Functor Stoneanᵒᵖ (Type (u + 1))) : CategoryTheory.Presieve.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] [CategoryTheory.ReflectsIsomorphisms G] (F : CategoryTheory.Functor Stoneanᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Functor.comp F 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] [CategoryTheory.ReflectsIsomorphisms G] (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] [CategoryTheory.ReflectsIsomorphisms G] (F : CategoryTheory.Functor Profiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F 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] [CategoryTheory.ReflectsIsomorphisms G] (F : CategoryTheory.Functor CompHausᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F 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 := ⋯ }

@[inline, reducible]

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

@[inline, reducible]

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

A CondensedSet version of Condensed.ofSheafProfinite. 

Equations

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

@[inline, reducible]

noncomputable abbrev CondensedSet.ofSheafCompHaus (F : CategoryTheory.Functor CompHausᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularCoverage.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.regularCoverage.EqualizerCondition X.val

A condensed set satisfies the equalizer condition.

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

A condensed set preserves finite products.

Equations

• CondensedSet.instPreservesFiniteProductsOppositeCompHausOppositeCategoryTypeTypesValCoherentTopologyProof_1 X = Nonempty.some ⋯

@[inline, reducible]

noncomputable abbrev CondensedAb.ofSheafStonean (F : CategoryTheory.Functor Stoneanᵒᵖ AddCommGroupCat) [CategoryTheory.Limits.PreservesFiniteProducts F] : CondensedAb

A CondensedAb version of Condensed.ofSheafStonean. 

Equations

• CondensedAb.ofSheafStonean F = Condensed.ofSheafStonean (CategoryTheory.forget AddCommGroupCat) F

@[inline, reducible]

noncomputable abbrev CondensedAb.ofSheafProfinite (F : CategoryTheory.Functor Profiniteᵒᵖ AddCommGroupCat) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat))) : CondensedAb

A CondensedAb version of Condensed.ofSheafProfinite. 

Equations

• CondensedAb.ofSheafProfinite F hF = Condensed.ofSheafProfinite (CategoryTheory.forget AddCommGroupCat) F hF

@[inline, reducible]

noncomputable abbrev CondensedAb.ofSheafCompHaus (F : CategoryTheory.Functor CompHausᵒᵖ AddCommGroupCat) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularCoverage.EqualizerCondition (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat))) : CondensedAb

A CondensedAb version of Condensed.ofSheafCompHaus. 

Equations

• CondensedAb.ofSheafCompHaus F hF = Condensed.ofSheafCompHaus (CategoryTheory.forget AddCommGroupCat) F hF