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.

Author: kckennylau

Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

@@ -35,12 +35,14 @@ namespace AlgebraicGeometry
 namespace Scheme
 
 /-- The Zariski pretopology on the category of schemes. -/
-def zariskiPretopology : Pretopology (Scheme.{u}) :=
+def zariskiPretopology : Pretopology Scheme.{u} :=
   pretopology @IsOpenImmersion
 
 /-- The Zariski topology on the category of schemes. -/
-abbrev zariskiTopology : GrothendieckTopology (Scheme.{u}) :=
-  zariskiPretopology.toGrothendieck
+abbrev zariskiTopology : GrothendieckTopology Scheme.{u} :=
+  grothendieckTopology IsOpenImmersion
+
+lemma zariskiTopology_eq : zariskiTopology.{u} = zariskiPretopology.toGrothendieck := rfl
 
 instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical := by
   apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj