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
    1. The counit of the discrete-underlying adjunction applied to X is an isomorphism
    2. X is in the essential image of the constant sheaf functor Type (u+1) ⥤ CondensedSet.{u}
    3. 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.
    4. The counit of the locally-constant-underlying adjunction applied to X is an isomorphism.
    5. X restricted to the coherent site of profinite sets is discrete as a sheaf
    6. 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

Estimated changes