[Merged by Bors] - feat(Condensed): discrete condensed sets are given by locally constant maps#15321
[Merged by Bors] - feat(Condensed): discrete condensed sets are given by locally constant maps#15321dagurtomas wants to merge 59 commits intomasterfrom
Conversation
… given by locally constant maps
PR summary 2ec7854e59Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Co-authored-by: Johan Commelin <johan@commelin.net>
| /-- `locallyConstantIsoContinuousMap` is a natural isomorphism. -/ | ||
| noncomputable def functorToPresheavesIsoTopCatToSheafCompHausLike (X : Type (max u w)) : | ||
| functorToPresheaves.{u, w}.obj X ≅ | ||
| ((topCatToSheafCompHausLike P hs).obj (TopCat.discrete.obj X)).val := |
There was a problem hiding this comment.
I'm going to merge this as is. But I think a follow-up PR could rename topCatToSheafCompHausLike to TopCat.toSheafCompHausLike. That would allow you to make several names a bit shorter.
There was a problem hiding this comment.
The name TopCat.toSheafCompHausLike already exists as the object part of that functor (which is more useful because of dot notation). But there are indeed some places in this file where that can be used, I opened #17075
…t 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.
|
Pull request successfully merged into master. Build succeeded: |
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 thesheaf 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.