Commit 2025-08-18 18:26 0436d526

View on Github →

chore(AlgebraicGeometry): change definition of Zariski topology (#28603) This PR changes the definition of the Zariski topology on Scheme from zariskiPretopology.toGrothendieck to grothendieckTopology IsOpenImmersion. Note that grothendieckTopology is an abbrev that uses toGrothendieck, so this definition should be strictly better and strictly unfolds to the old definition.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

modified def AlgebraicGeometry.Scheme.zariskiPretopology

added theorem AlgebraicGeometry.Scheme.zariskiTopology_eq