Commit 2024-10-17 08:31 21bb8348
View on Github →feat(Condensed): characterisation of discrete (light) condensed sets and modules (#14027) This PR provides a characterization of discrete condensed sets and modules, both in the light setting and the classical one.
- Six equivalent conditions on a condensed set X to be discrete
- The counit of the discrete-underlying adjunction applied to X is an isomorphism
- X is in the essential image of the constant sheaf functor
Type (u+1) ⥤ CondensedSet.{u}
- X is in the essential image of the functor
Type (u+1) ⥤ CondensedSet.{u}
which takes a set to the sheaf of locally constant maps into it. - The counit of the locally-constant-underlying adjunction applied to X is an isomorphism.
- X restricted to the coherent site of profinite sets is discrete as a sheaf
- For every profinite set S written as a limit of finite sets, X maps S to the corresponding colimit.
- A condensed module over a ring is discrete if and only if its underlying condensed set is, and therefore the analogues of the equivalent conditions above also characterize condensed modules as discrete
- The analogues for the above for light condensed sets and modules