Documentation Verification Report

BigZariski

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

Statistics

Metric	Count
Definitions `affineOneHypercover`, `zariskiPretopology`, `zariskiTopology`	3
Theorems `isSheafFor_sigma_iff`, `affineOneHypercover_toPreOneHypercover_toPreZeroHypercover`, `instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology`, `subcanonical_zariskiTopology`, `zariskiTopology_eq`, `ofArrows_ι_mem_zariskiTopology_of_isColimit`, `preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology`	7
Total	10

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofArrows_ι_mem_zariskiTopology_of_isColimit` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Functor.obj` `Scheme` `Scheme.instCategory` `CategoryTheory.Functor.map` `Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Sieve` `Scheme` `Scheme.instCategory` `Set` `CategoryTheory.Limits.Cocone.pt` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `Scheme.zariskiTopology` `CategoryTheory.Sieve.ofArrows` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι`	—	`Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.Sieve.ofArrows.eq_1` `CategoryTheory.Sieve.generate_le_iff` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv` `Scheme.Cover.mem_grothendieckTopology`
`preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf` `Scheme` `Scheme.instCategory` `Scheme.zariskiTopology`	`CategoryTheory.Limits.PreservesLimitsOfShape` `Opposite` `Scheme` `CategoryTheory.Category.opposite` `Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Limits.preservesLimitsOfShape_of_discrete` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Presieve.preservesProduct_of_isSheafFor` `instHasInitialScheme` `CategoryTheory.Presieve.IsSheaf.isSheafFor` `Empty.instIsEmpty` `eq_bot_iff` `Scheme.bot_mem_grothendieckTopology` `initial_isEmpty` `CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks` `Scheme.Pullback.instHasPullbacks` `CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial` `CategoryTheory.Limits.CoproductsOfShapeDisjoint.coproductDisjoint` `instCoproductsOfShapeDisjointSchemeOfSmall` `Scheme.Pullback.instHasPullback` `Scheme.Cover.mem_grothendieckTopology`

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`affineOneHypercover` 📖	CompOp	1 math math: `affineOneHypercover_toPreOneHypercover_toPreZeroHypercover`
`zariskiPretopology` 📖	CompOp	1 math math: `zariskiTopology_eq`
`zariskiTopology` 📖	CompOp	31 math math: `GlueData.oneHypercover_I₁`, `zariskiTopology_le_etaleTopology`, `zariskiTopology_eq`, `LocalRepresentability.isRepresentable`, `zariskiTopology_le_fpqcTopology`, `LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`, `AlgebraicGeometry.isSheaf_propQCTopology_iff`, `instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology`, `AlgebraicGeometry.isSheaf_type_propQCTopology_iff`, `LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc`, `GlueData.oneHypercover_p₂`, `LocalRepresentability.glueData_V`, `GlueData.sheafValGluedMk_val`, `LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf`, `LocalRepresentability.glueData_f`, `LocalRepresentability.glueData_t'`, `LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf`, `LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf`, `GlueData.oneHypercover_X`, `AlgebraicGeometry.ofArrows_ι_mem_zariskiTopology_of_isColimit`, `LocalRepresentability.yonedaGluedToSheaf_app_comp`, `GlueData.oneHypercover_I₀`, `LocalRepresentability.glueData_t`, `GlueData.oneHypercover_f`, `GlueData.oneHypercover_Y`, `zariskiTopology_le_propQCTopology`, `GlueData.oneHypercover_p₁`, `affineOneHypercover_toPreOneHypercover_toPreZeroHypercover`, `AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf`, `subcanonical_zariskiTopology`, `LocalRepresentability.yonedaGluedToSheaf_app_toGlued`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineOneHypercover_toPreOneHypercover_toPreZeroHypercover` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `zariskiTopology` `affineOneHypercover` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `AlgebraicGeometry.IsOpenImmersion` `affineCover`	—	—
`instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.Functor.IsContinuous` `AlgebraicGeometry.Scheme` `instCategory` `TopCat` `TopCat.instCategory` `forgetToTop` `zariskiTopology` `TopCat.grothendieckTopology`	—	`zariskiTopology.eq_1` `grothendieckTopology.eq_1` `AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop` `CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy` `instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `instHasPullbacksPrecoverageOfHasPullbacks` `instHasPullbacksIsOpenImmersion` `CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `TopCat.topCat_hasLimits` `TopCat.precoverage.eq_1` `CategoryTheory.Precoverage.comap_inf` `precoverage.eq_1` `inf_le_inf` `CategoryTheory.Precoverage.comap_comp` `forgetToTop_comp_forget` `le_refl` `CategoryTheory.MorphismProperty.comap_precoverage` `CategoryTheory.MorphismProperty.precoverage_monotone` `Hom.isOpenEmbedding`
`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`

AlgebraicGeometry.Scheme.Cover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafFor_sigma_iff` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.Presieve.IsSheafFor` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Presieve.ofArrows` `CategoryTheory.PreZeroHypercover.I₀` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `sigma` `univLE_of_max` `UnivLE.self` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f`	—	`AlgebraicGeometry.preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology` `small_prod` `UnivLE.small` `UnivLE.self` `Countable.toSmall` `Finite.to_countable` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `univLE_of_max` `CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff` `CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.IsVanKampenColimit.isUniversal` `CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts` `AlgebraicGeometry.instFinitaryExtensiveScheme` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows` `CategoryTheory.PreZeroHypercover.presieve₀.eq_1` `presieve₀_sigma`

---

← Back to Index