Commit 2024-07-01 13:36 a94c84c7

feat: quasi-coherent sheaves (#13464) In this PR, we define the notion of quasi-coherent sheaf: a sheaf of modules M over a sheaf of rings R (on a category C equipped with a Grothendieck topology) is quasi-coherent if, locally, it admits a presentation involving coproducts of copies of the restriction of R. We also introduce the notions of sheaves of modules of finite type/presentation. These are only definitions. No attempt is made yet to prove anything about this notion in the case of schemes!