Commit 2024-07-04 12:51 ac0ca966

feat(CategoryTheory/Sites): functors preserving 1-hypercovers are continuous (#13012) Given a functor F : C ⥤ D between categories equipped with Grothendieck topologies, the condition that F preserves covers (developed in the file CategoryTheory.Sites.CoverPreserving) does not obviously imply that F is a continuous functor (i.e. the precomposition with F.op of a sheaf is a sheaf). However, it becomes obvious if we require that F preserves 1-hypercovers of a suitable size. The general definitions involving continuous functors have been moved from Sites.CoverPreserving to a new file Sites.Continuous.