Commit 2025-09-19 16:11 d9cecd1c

View on Github →

refactor(AlgebraicGeometry): rename fields of Scheme.Cover to match ZeroHypercover (#29803) This is in preparation for replacing Scheme.Cover by ZeroHypercover for the Zariski precoverage (see #29061). For consistency, also the fields of Scheme.AffineCover were updated accordingly. Deprecations were added for the following renames:

  • Scheme.Cover.J -> Scheme.Cover.I₀
  • Scheme.Cover.obj -> Scheme.Cover.X
  • Scheme.Cover.map -> Scheme.Cover.f and similarly for AffineCover. No deprecations were added for the automatically generated simps lemmas, in the expectation that users will already get a deprecation warning for one of the fields above.

Estimated changes

modified structure AlgebraicGeometry.Scheme.Cover