Commit 2025-08-28 14:45 39955fe0

feat(AlgebraicGeometry): directed covers (#24528) Directed covers are covers, where every intersection can be covered by a component of the cover. For open covers this is equivalent to the images forming a basis of the topology. If a cover is directed, the compatibility conditions for gluing become easier, because only compatibility with the transition maps needs to be checked. In particular, the covered scheme naturally is the colimit of the components of the cover.