Commit 2024-10-04 11:14 7b3092eb

feat(Condensed): discrete condensed modules are given by locally constant maps (#15569) This PR provides the necessary API to prove that a condensed R-module is discrete if and only if the underlying condensed set is (both for light condensed and condensed). That is, it defines the functor CondensedMod.LocallyConstant.functor which takes an R-module to the condensed R-modules given by locally constant maps to it, and proves that this functor is naturally isomorphic to the constant sheaf functor (and the analogues for light condensed modules). The actual result that a condensed module is discrete if and only if the underlying condensed set is follows easily and is added in #14027.