Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.zariskiTopology

CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme

The Zariski topology on the category of schemes.

Defined in
Mathlib.AlgebraicGeometry.Sites.BigZariski
Cited by
34 results in Mathlib
Foundations
Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Scheme.LocalRepresentability.glueData · cited by 13LocalRepresentability.glu…AlgebraicGeometry.Scheme.GlueData.oneHypercover · cited by 8GlueData.oneHypercoverAlgebraicGeometry.Scheme.LocalRepresentability.toGlued · cited by 5LocalRepresentability.toG…AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf · cited by 4LocalRepresentability.yon…AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk · cited by 3GlueData.sheafValGluedMkAlgebraicGeometry.Scheme.affineOneHypercover · cited by 2Scheme.affineOneHypercoverAlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf · cited by 2LocalRepresentability.yon…AlgebraicGeometry.Scheme.LocalRepresentability.representableBy · cited by 1LocalRepresentability.rep…AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val · cited by 1GlueData.sheafValGluedMk_…AlgebraicGeometry.preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology · cited by 1AlgebraicGeometry.preserv…AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff · cited by 1Cover.isSheafFor_sigma_iffAlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology · cited by 1Scheme.zariskiTopology_le…AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf · cited by 1AlgebraicGeometry.isSheaf…AlgebraicGeometry.isSheaf_type_propQCTopology_iff · cited by 1AlgebraicGeometry.isSheaf…AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf · cited by 1AlgebraicGeometry.isSheaf…AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.GrothendieckTopology · cited by 1415CategoryTheory.Grothendie…AlgebraicGeometry.IsOpenImmersion · cited by 476AlgebraicGeometry.IsOpenI…AlgebraicGeometry.Scheme.grothendieckTopology · cited by 7Scheme.grothendieckTopolo…Scheme.zariskiTopologyCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by42

Results whose statement or proof uses this declaration.