Commit 2024-09-24 05:56 88dd555b

feat(Condensed): discrete condensed sets are given by locally constant maps (#15321) This PR proves that under suitable conditions, the functor from the category of sets to the category of sheaves for the coherent topology on CompHausLike P, given by mapping a set to the sheaf of locally constant maps to it, is left adjoint to the "underlying set" functor (evaluation at the point). We apply this to prove that the constant sheaf functor into (light) condensed sets is isomorphic to the functor of sheaves of locally constant maps described above. This is the first part of the characterization of discrete condensed objects, see #14027.