Commit 2024-07-15 20:56 60213779

feat(CategoryTheory/Sites): discrete sheaves (#13947) This PR defines the property of discreteness for sheaves. A discrete sheaf in this context is a sheaf F such that the counit (F(*))^cst ⟶ F is an isomorphism. Here * denotes a particular chosen terminal object of the defining site, and cst denotes the constant sheaf. We also prove that this property is invariant under equivalence of categories and that certain well-behaved "forgetful" functors preserve and reflect the property.