Commit 2024-07-15 19:24 f80e4f06

feat(AlgebraicGeometry): the 1-hypercover attached to a GlueData (#14690) Given D : Scheme.GlueData, we define the 1-hypercover of the scheme D.glued on the big Zariski site and use it in order to define a constructor for sections over D.glued of a sheaf of types over the big Zariski site. (Incidentally, the lemma Sieve.sets_iff_generate is renamed Sieve.generate_le_iff.) This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.