Commit 2025-03-27 18:01 0beb5de9

feat(AlgebraicGeometry): representability by a scheme is a local property (#14208) The purpose of this PR is to prove the representability theorem https://stacks.math.columbia.edu/tag/01JJ It says that if a sheaf of types on the big Zariski site of schemes is covered by representable open subfunctors, then it is representable by a scheme. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.