Commit 2025-10-03 06:19 6dcfd42a
View on Github →refactor(AlgebraicGeometry): replace Scheme.Cover by an abbrev for ZeroHypercover (#29061)
We replace Scheme.Cover by an abbrev for Coverage.ZeroHypercover. The main motivation is to allow for a generalization of IsLocalAtTarget, IsLocalAtSource etc. to arbitrary coverages. The second motivation is to reduce duplication in the upcoming introduction of categories of analytic spaces (e.g. adic spaces), by generalizing notions of Cover to suitable general categories.
Future work: Besides the generalisation of IsLocalAtTarget, the content of AlgebraicGeometry.Cover.Over and AlgebraicGeometry.Sites.Small shall be generalized to general coverages instead of the coverage induced by a morphism property.