Characterizing discrete condensed sets and R-modules.

This file proves a characterization of discrete condensed sets, discrete condensed R-modules over a ring R, discrete light condensed sets, and discrete light condensed R-modules over a ring R. see CondensedSet.isDiscrete_tfae, CondensedMod.isDiscrete_tfae, LightCondSet.isDiscrete_tfae, and LightCondMod.isDiscrete_tfae.

Informally, we can say: The following conditions characterize a condensed set X as discrete (CondensedSet.isDiscrete_tfae):

1. There exists a set X' and an isomorphism X ≅ cst X', where cst X' denotes the constant sheaf on X'.
2. The counit induces an isomorphism cst X(*) ⟶ X.
3. There exists a set X' and an isomorphism X ≅ LocallyConstant · X'.
4. The counit induces an isomorphism LocallyConstant · X(*) ⟶ X.
5. For every profinite set S = limᵢSᵢ, the canonical map colimᵢX(Sᵢ) ⟶ X(S) is an isomorphism.

The analogues for light condensed sets, condensed R-modules over any ring, and light condensed R-modules are nearly identical (CondensedMod.isDiscrete_tfae, LightCondSet.isDiscrete_tfae, and LightCondMod.isDiscrete_tfae).

@[reducible, inline]

abbrev Condensed.IsDiscrete {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] (X : Condensed C) : Prop

A condensed object is discrete if it is constant as a sheaf, i.e. isomorphic to a constant sheaf.

Equations

• X.IsDiscrete = CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology CompHaus) X

theorem CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone (X : CondensedSet) (h : (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op)) : LocallyConstant.functor.essImage X

@[deprecated CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone (since := "2024-12-25")]

theorem CondensedSet.mem_locallyContant_essImage_of_isColimit_mapCocone (X : CondensedSet) (h : (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op)) : LocallyConstant.functor.essImage X

Alias of CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone.

@[reducible, inline]

noncomputable abbrev CondensedSet.LocallyConstant.adjunction : functor ⊣ Condensed.underlying (Type (u + 1))

CondensedSet.LocallyConstant.functor is left adjoint to the forgetful functor from condensed sets to sets.

Equations

• CondensedSet.LocallyConstant.adjunction = CompHausLike.LocallyConstant.adjunction (fun (x : TopCat) => True) CondensedSet.LocallyConstant.functor._proof_1

theorem CondensedSet.isDiscrete_tfae (X : CondensedSet) : [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X), (Condensed.discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X, CategoryTheory.IsIso (LocallyConstant.adjunction.counit.app X), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op))].TFAE

theorem CondensedMod.isDiscrete_iff_isDiscrete_forget (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : Condensed.IsDiscrete M ↔ Condensed.IsDiscrete ((Condensed.forget R).obj M)

instance CondensedMod.instHasLimitsOfSizeModuleCat (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)

theorem CondensedMod.isDiscrete_tfae (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (Condensed.discrete (ModuleCat R)).essImage M, (LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((LocallyConstant.adjunction R).counit.app M), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.val).mapCocone S.asLimitCone.op))].TFAE

@[reducible, inline]

abbrev LightCondensed.IsDiscrete {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology LightProfinite) C] (X : LightCondensed C) : Prop

A light condensed object is discrete if it is constant as a sheaf, i.e. isomorphic to a constant sheaf.

Equations

• X.IsDiscrete = CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology LightProfinite) X

theorem LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone (X : LightCondSet) (h : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : LocallyConstant.functor.essImage X

@[deprecated LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone (since := "2024-12-25")]

theorem LightCondSet.mem_locallyContant_essImage_of_isColimit_mapCocone (X : LightCondSet) (h : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : LocallyConstant.functor.essImage X

Alias of LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone.

@[reducible, inline]

noncomputable abbrev LightCondSet.LocallyConstant.adjunction : functor ⊣ LightCondensed.underlying (Type u)

LightCondSet.LocallyConstant.functor is left adjoint to the forgetful functor from light condensed sets to sets.

Equations

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

theorem LightCondSet.isDiscrete_tfae (X : LightCondSet) : [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X), (LightCondensed.discrete (Type u)).essImage X, LocallyConstant.functor.essImage X, CategoryTheory.IsIso (LocallyConstant.adjunction.counit.app X), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (X.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE

theorem LightCondMod.isDiscrete_iff_isDiscrete_forget (R : Type u) [Ring R] (M : LightCondMod R) : LightCondensed.IsDiscrete M ↔ LightCondensed.IsDiscrete ((LightCondensed.forget R).obj M)

theorem LightCondMod.isDiscrete_tfae (R : Type u) [Ring R] (M : LightCondMod R) : [LightCondensed.IsDiscrete M, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (LightCondensed.discrete (ModuleCat R)).essImage M, (LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((LocallyConstant.adjunction R).counit.app M), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (M.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE