Commit 2023-11-25 10:19 5ddf761e

feat(AlgebraicGeometry): the big Zariski site (#8549) This PR defines the Zariski topology on the category of schemes. It may have some applications, but it should also be considered as a test case for the Grothendieck topologies API in order to check that is general enough, in particular in terms of universes: a priori, the category which shall form the small étale site of a scheme will have the same universe parameters.