Documentation Verification Report

Small

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

Statistics

Metric	Count
Definitions `toPresieveOver`, `toPresieveOverProp`, `overGrothendieckTopology`, `overPretopology`, `smallGrothendieckTopology`, `smallGrothendieckTopologyOfLE`, `smallPretopology`	7
Theorems `overEquiv_generate_toPresieveOver_eq_ofArrows`, `toPresieveOver_le_arrows_iff`, `instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology`, `locallyCoverDense_of_le`, `mem_overGrothendieckTopology`, `mem_smallGrothendieckTopology`, `mem_toGrothendieck_smallPretopology`, `overGrothendieckTopology_eq_toGrothendieck_overPretopology`, `smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology`, `smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`	10
Total	17

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`overGrothendieckTopology` 📖	CompOp	4 math math: `overGrothendieckTopology_eq_toGrothendieck_overPretopology`, `locallyCoverDense_of_le`, `mem_overGrothendieckTopology`, `instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology`
`overPretopology` 📖	CompOp	1 math math: `overGrothendieckTopology_eq_toGrothendieck_overPretopology`
`smallGrothendieckTopology` 📖	CompOp	2 math math: `smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`, `mem_smallGrothendieckTopology`
`smallGrothendieckTopologyOfLE` 📖	CompOp	1 math math: `smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology`
`smallPretopology` 📖	CompOp	3 math math: `smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology`, `smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`, `mem_toGrothendieck_smallPretopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.Functor.LocallyCoverDense` `CategoryTheory.MorphismProperty.Over` `AlgebraicGeometry.Scheme` `instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over.forget` `overGrothendieckTopology`	—	`locallyCoverDense_of_le` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `le_rfl`
`locallyCoverDense_of_le` 📖	mathematical	`CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`CategoryTheory.Functor.LocallyCoverDense` `CategoryTheory.MorphismProperty.Over` `Top.top` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over.forget` `overGrothendieckTopology`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isJointlySurjectivePreserving` `mem_overGrothendieckTopology` `CategoryTheory.comp_over` `Cover.Over.isOver_map` `CategoryTheory.MorphismProperty.comp_mem` `Cover.map_prop` `CategoryTheory.MorphismProperty.Comma.prop`
`mem_overGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.Sieve` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.instCategoryOver` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `overGrothendieckTopology` `CategoryTheory.Presieve` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CategoryTheory.instCompleteLatticePresieve` `Cover.toPresieveOver` `CategoryTheory.Sieve.arrows`	—	`isJointlySurjectivePreserving` `CategoryTheory.Over.instHasPullbacks` `Pullback.instHasPullbacks` `overGrothendieckTopology_eq_toGrothendieck_overPretopology`
`mem_smallGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.Sieve` `CategoryTheory.MorphismProperty.Over` `AlgebraicGeometry.Scheme` `instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `smallGrothendieckTopology` `CategoryTheory.Presieve` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CategoryTheory.instCompleteLatticePresieve` `Cover.toPresieveOverProp` `CategoryTheory.Sieve.arrows`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isJointlySurjectivePreserving` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`
`mem_toGrothendieck_smallPretopology` 📖	mathematical	—	`CategoryTheory.Sieve` `CategoryTheory.MorphismProperty.Over` `AlgebraicGeometry.Scheme` `instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Pretopology.toGrothendieck` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `smallPretopology` `CategoryTheory.Sieve.arrows` `CategoryTheory.Comma.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `CategoryTheory.Pretopology.mem_toGrothendieck` `isJointlySurjectivePreserving` `instJointlySurjectivePrecoverage` `Cover.covers` `Cover.Over.isOver_map` `CategoryTheory.MorphismProperty.Comma.prop` `Cover.map_prop` `presieve₀_mem_precoverage_iff` `CategoryTheory.instHomIsOverLeftDiscretePUnit`
`overGrothendieckTopology_eq_toGrothendieck_overPretopology` 📖	mathematical	—	`overGrothendieckTopology` `CategoryTheory.Pretopology.toGrothendieck` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.instHasPullbacks` `Pullback.instHasPullbacks` `overPretopology`	—	`CategoryTheory.GrothendieckTopology.ext` `CategoryTheory.Over.instHasPullbacks` `Pullback.instHasPullbacks` `Set.ext` `CategoryTheory.GrothendieckTopology.mem_over_iff` `exists_cover_of_mem_grothendieckTopology` `isJointlySurjectivePreserving` `Cover.toPresieveOver_le_arrows_iff` `mem_grothendieckTopology_iff`
`smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology` 📖	mathematical	`CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`smallGrothendieckTopologyOfLE` `CategoryTheory.Pretopology.toGrothendieck` `CategoryTheory.MorphismProperty.Over` `Top.top` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `smallPretopology`	—	`CategoryTheory.GrothendieckTopology.ext` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `Set.ext` `isJointlySurjectivePreserving` `locallyCoverDense_of_le` `CategoryTheory.comp_over` `Cover.Over.isOver_map` `CategoryTheory.MorphismProperty.comp_mem` `Cover.map_prop` `CategoryTheory.MorphismProperty.Comma.prop` `CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful` `CategoryTheory.MorphismProperty.instFullOverTopOverForget` `CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget` `CategoryTheory.Sieve.functorPushforward_apply`
`smallGrothendieckTopology_eq_toGrothendieck_smallPretopology` 📖	mathematical	—	`smallGrothendieckTopology` `CategoryTheory.Pretopology.toGrothendieck` `CategoryTheory.MorphismProperty.Over` `AlgebraicGeometry.Scheme` `instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `smallPretopology`	—	`smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `le_rfl`

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
`toPresieveOver` 📖	CompOp	3 math math: `AlgebraicGeometry.Scheme.mem_overGrothendieckTopology`, `toPresieveOver_le_arrows_iff`, `overEquiv_generate_toPresieveOver_eq_ofArrows`
`toPresieveOverProp` 📖	CompOp	1 math math: `AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`overEquiv_generate_toPresieveOver_eq_ofArrows` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Sieve` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.instCategoryOver` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Sieve.overEquiv` `CategoryTheory.Sieve.generate` `toPresieveOver` `CategoryTheory.Sieve.ofArrows` `CategoryTheory.PreZeroHypercover.I₀` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f`	—	`AlgebraicGeometry.Scheme.isJointlySurjectivePreserving` `CategoryTheory.Sieve.ext` `CategoryTheory.comp_over` `Over.isOver_map` `CategoryTheory.Category.assoc` `CategoryTheory.Over.OverMorphism.ext`
`toPresieveOver_le_arrows_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.instCategoryOver` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CategoryTheory.instCompleteLatticePresieve` `toPresieveOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Presieve.ofArrows` `CategoryTheory.PreZeroHypercover.I₀` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.PreZeroHypercover.f` `DFunLike.coe` `Equiv` `CategoryTheory.Sieve` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Sieve.overEquiv`	—	`AlgebraicGeometry.Scheme.isJointlySurjectivePreserving` `GaloisConnection.le_iff_le` `GaloisInsertion.gc` `overEquiv_generate_toPresieveOver_eq_ofArrows`

---

← Back to Index