Documentation Verification Report

BigZariski

📁 Source: Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

Statistics

Metric	Count
Definitions `zariskiPretopology`, `zariskiTopology`	2
Theorems `subcanonical_zariskiTopology`, `zariskiTopology_eq`	2
Total	4

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`zariskiPretopology` 📖	CompOp	1 math math: `zariskiTopology_eq`
`zariskiTopology` 📖	CompOp	10 math math: `GlueData.oneHypercover_I₁`, `zariskiTopology_le_etaleTopology`, `zariskiTopology_eq`, `GlueData.oneHypercover_p₂`, `GlueData.oneHypercover_X`, `GlueData.oneHypercover_I₀`, `GlueData.oneHypercover_f`, `GlueData.oneHypercover_Y`, `GlueData.oneHypercover_p₁`, `subcanonical_zariskiTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subcanonical_zariskiTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.Subcanonical` `AlgebraicGeometry.Scheme` `instCategory` `zariskiTopology`	—	`CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj` `CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange` `instHasPullbacksPrecoverageOfHasPullbacks` `instHasPullbacksIsOpenImmersion` `instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `exists_cover_of_mem_pretopology` `AlgebraicGeometry.isOpenImmersion_isMultiplicative` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right` `instIsOpenImmersionF` `CategoryTheory.Limits.pullback.condition` `Cover.ι_glueMorphisms` `Cover.hom_ext`
`zariskiTopology_eq` 📖	mathematical	—	`zariskiTopology` `CategoryTheory.Pretopology.toGrothendieck` `AlgebraicGeometry.Scheme` `instCategory` `Pullback.instHasPullbacks` `zariskiPretopology`	—	`Pullback.instHasPullbacks` `instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `AlgebraicGeometry.isOpenImmersion_isMultiplicative` `AlgebraicGeometry.isOpenImmersion_respectsIso` `instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck`

---

← Back to Index