Commit 2026-02-09 11:07 6045d6f5

View on Github →

chore(AlgebraicGeometry/Sites): use Precoverage.toGrothendieck instead of Pretopology.toGrothendieck (#34995) As more and more API is developed in terms of Precoverages and Precoverage.toGrothendieck, this makes application of the general category theory library easier. We also add a few additional API lemmas.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

modified theorem AlgebraicGeometry.Scheme.zariskiTopology_eq

Modified Mathlib/AlgebraicGeometry/Sites/Etale.lean

added def AlgebraicGeometry.Scheme.etalePrecoverage

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

added theorem AlgebraicGeometry.Scheme.bot_mem_precoverage

added theorem AlgebraicGeometry.Scheme.precoverage_mono

Modified Mathlib/AlgebraicGeometry/Sites/Pretopology.lean

modified theorem AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology

added theorem AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology

modified theorem AlgebraicGeometry.Scheme.pretopology_monotone

Modified Mathlib/AlgebraicGeometry/Sites/Small.lean