The explicit sheaf condition for light condensed sets

We give explicit description of light condensed sets:

• LightCondensed.ofSheafLightProfinite: A finite-product-preserving presheaf on LightProfinite, 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)

We also give variants for light 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.

@[simp]

theorem LightCondensed.ofSheafLightProfinite_val {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : (LightCondensed.ofSheafLightProfinite F hF).val = F

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

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

Equations

• LightCondensed.ofSheafLightProfinite F hF = { val := F, cond := ⋯ }

@[simp]

theorem LightCondensed.ofSheafForgetLightProfinite_val {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A))) : (LightCondensed.ofSheafForgetLightProfinite F hF).val = F

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

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

Equations

• LightCondensed.ofSheafForgetLightProfinite F hF = { val := F, cond := ⋯ }

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

A light condensed object satisfies the equalizer condition.

noncomputable instance LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] (X : LightCondensed A) : CategoryTheory.Limits.PreservesFiniteProducts X.val

A light condensed object preserves finite products.

Equations

• X.instPreservesFiniteProductsOppositeLightProfiniteVal = ⋯.some

@[reducible, inline]

noncomputable abbrev LightCondSet.ofSheafLightProfinite (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : LightCondSet

A LightCondSet version of LightCondensed.ofSheafLightProfinite. 

Equations

• LightCondSet.ofSheafLightProfinite F hF = LightCondensed.ofSheafLightProfinite F hF

@[reducible, inline]

noncomputable abbrev LightCondMod.ofSheafLightProfinite (R : Type u) [Ring R] (F : CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : LightCondMod R

A LightCondAb version of LightCondensed.ofSheafLightProfinite. 

Equations

• LightCondMod.ofSheafLightProfinite R F hF = LightCondensed.ofSheafLightProfinite F hF

@[reducible, inline]

noncomputable abbrev LightCondAb.ofSheafLightProfinite (F : CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat ℤ)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F) : LightCondAb

A LightCondAb version of LightCondensed.ofSheafLightProfinite. 

Equations

• LightCondAb.ofSheafLightProfinite F hF = LightCondMod.ofSheafLightProfinite ℤ F hF