Commit 2026-01-14 20:45 25d72f3b
View on Github →refactor(AlgebraicGeometry/Cover): make Scheme.Cover.Hom an abbrev for ZeroHypercover.Hom (#33937)
This slightly changes the meaning of Scheme.Cover.Hom (precoverage P), because the old definition required the transition maps to satisfy P (where P is a morphism property of schemes). In the general definition, this condition does not make sense.
The meaning remains unchanged for every P that satisfies a suitable cancellation property (HasOfPostcompProperty), in particular for open covers.