Documentation Verification Report

IsSheaf

📁 Source: Mathlib/CategoryTheory/Sites/Hypercover/IsSheaf.lean

Statistics

Metric	Count
Definitions `IsGeneratedByOneHypercovers`, `OneHypercoverFamily`, `IsGenerating`, `isLimit`, `IsSheaf`, `IsSheaf`, `IsSheaf`	7
Theorems `IsSheaf`, `le`, `fac`, `fac'`, `fac'_assoc`, `hom_ext`, `exists_oneHypercover`, `isSheaf_iff`, `instIsGeneratedByOneHypercovers`, `isSheaf_iff_of_isGeneratedByOneHypercovers`	10
Total	17

AlgebraicGeometry.SheafedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsSheaf` 📖	mathematical	—	`TopCat.Presheaf.IsSheaf` `AlgebraicGeometry.PresheafedSpace.carrier` `toPresheafedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf`	—	—

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`IsGeneratedByOneHypercovers` 📖	MathDef	1 math math: `instIsGeneratedByOneHypercovers`
`OneHypercoverFamily` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsGeneratedByOneHypercovers` 📖	mathematical	—	`IsGeneratedByOneHypercovers`	—	`Cover.preOneHypercover_sieve₀`

CategoryTheory.GrothendieckTopology.OneHypercoverFamily

Definitions

Name	Category	Theorems
`IsGenerating` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_oneHypercover` 📖	mathematical	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.PreZeroHypercover.sieve₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover`	—	`IsGenerating.le`
`isSheaf_iff` 📖	mathematical	—	`CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork`	—	`CategoryTheory.Presheaf.isSheaf_iff_multifork` `exists_oneHypercover`

CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le` 📖	mathematical	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.PreZeroHypercover.sieve₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover`	—	—

CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff

Definitions

Name	Category	Theorems
`isLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork` `CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.PreZeroHypercover.sieve₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `CategoryTheory.Sieve.arrows`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.GrothendieckTopology.Cover.shape` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `lift` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.Multifork.ι`	—	`CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `hom_ext` `CategoryTheory.GrothendieckTopology.pullback_stable` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `fac'_assoc` `CategoryTheory.Limits.Multifork.condition`
`fac'` 📖	mathematical	`CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork` `CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.PreZeroHypercover.sieve₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.GrothendieckTopology.Cover.shape` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.PreZeroHypercover.X` `lift` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Limits.Multifork.ι` `CategoryTheory.PreZeroHypercover.I₀`	—	`CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `CategoryTheory.Limits.Multifork.IsLimit.fac`
`fac'_assoc` 📖	mathematical	`CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork` `CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.PreZeroHypercover.sieve₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.GrothendieckTopology.Cover.shape` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `lift` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Limits.Multifork.ι` `CategoryTheory.PreZeroHypercover.I₀`	—	`CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.GrothendieckTopology.OneHypercover.mem₀` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac'`
`hom_ext` 📖	—	`CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork` `CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	—	`CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover` `CategoryTheory.Limits.Multifork.IsLimit.hom_ext`

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
`IsSheaf` 📖	MathDef	43 math math: `CategoryTheory.Equivalence.preregular_isSheaf_iff`, `isSheaf_of_isTerminal`, `CategoryTheory.ran_isSheaf_of_isCocontinuous`, `isSheaf_iff_isLimit_coverage`, `CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall`, `CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff`, `isSheaf_of_iso_iff`, `isSheaf_iff_preservesFiniteProducts`, `isSheaf_iff_preservesFiniteProducts_and_equalizerCondition`, `Condensed.isSheafStonean`, `isSheaf_yoneda'`, `CategoryTheory.Sheaf.tensorProd_isSheaf`, `SheafOfModules.isSheaf`, `isSheaf_coherent_iff_regular_and_extensive`, `isSheaf_iff_extensiveSheaf_of_projective`, `CategoryTheory.regularTopology.isSheaf_of_projective`, `isSheaf_iff_of_isGeneratedByOneHypercovers`, `isSheaf_iff_isSheaf'`, `CategoryTheory.Sheaf.isSheaf_of_isLimit`, `CategoryTheory.isSheaf_pointwiseColimit`, `CategoryTheory.Sheaf.cond`, `Topology.IsUpperSet.isSheaf_of_isRightKanExtension`, `CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf`, `isSheaf_iff_isLimit`, `isSheaf_iff_multiequalizer`, `CategoryTheory.GrothendieckTopology.sheafify_isSheaf`, `isSheaf_iff_multifork`, `isSheaf_iff_preservesFiniteProducts_of_projective`, `CategoryTheory.isSheaf_iff_isSheaf_of_type`, `CategoryTheory.Equivalence.precoherent_isSheaf_iff`, `isSheaf_bot`, `CategoryTheory.Pseudofunctor.IsPrestack.isSheaf`, `isSheaf_iff_isSheaf_comp`, `CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus`, `CategoryTheory.Functor.op_comp_isSheaf`, `CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep`, `CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall`, `isSheaf_iff_isSheaf_forget`, `CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff`, `Condensed.isSheafProfinite`, `isSheaf_sup`, `CategoryTheory.Sheaf.tensorUnit_isSheaf`, `isSheaf_iff_isLimit_pretopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_iff_of_isGeneratedByOneHypercovers` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork`	—	`CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff`

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
`IsSheaf` 📖	MathDef	26 math math: `isSheaf_pretopology`, `isSheaf_iff_preservesFiniteProducts`, `isSheaf_bot`, `isSheaf_iff_of_nat_equiv`, `CategoryTheory.extensiveTopology.isSheaf_yoneda_obj`, `CategoryTheory.topology_eq_iff_same_sheaves`, `CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small`, `CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff`, `CategoryTheory.Functor.op_comp_isSheaf_of_types`, `isSheaf_of_yoneda`, `CategoryTheory.regularTopology.isSheaf_yoneda_obj`, `CategoryTheory.coherentTopology.isSheaf_yoneda_obj`, `CategoryTheory.Sheaf.sheaf_for_finestTopology`, `CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable`, `CategoryTheory.isSheaf_iff_isSheaf_of_type`, `isSheaf_coverage`, `IsSeparated.isSheaf`, `CategoryTheory.isSheaf_coherent`, `CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types`, `isSheaf_yoneda'`, `isSheaf_comp_uliftFunctor_iff`, `CategoryTheory.classifier_isSheaf`, `CategoryTheory.Sheaf.isSheaf_of_isRepresentable`, `CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange`, `isSheaf_sup`, `CategoryTheory.Sheaf.isSheaf_yoneda_obj`

TopCat.Presheaf

Definitions

Name	Category	Theorems
`IsSheaf` 📖	MathDef	22 math math: `isSheaf_of_isTerminal_of_indiscrete`, `isSheaf_iff_isSheafUniqueGluing_types`, `isSheaf_iff_isSheafPairwiseIntersections`, `isSheaf_iff_isSheafPreservesLimitPairwiseIntersections`, `AlgebraicGeometry.Scheme.Modules.isSheaf`, `isSheaf_iff_isSheaf_comp`, `isSheaf_of_isSheafUniqueGluing_types`, `isSheaf_iff_isSheafOpensLeCover`, `AlgebraicGeometry.SheafedSpace.IsSheaf`, `isSheaf_on_punit_of_isTerminal`, `TopCat.subpresheafToTypes.isSheaf`, `isSheaf_on_punit_iff_isTerminal`, `isSheaf_iff_isSheaf_comp'`, `isSheaf_unit`, `skyscraperPresheaf_isSheaf`, `isSheaf_iff_isSheafUniqueGluing`, `toTypes_isSheaf`, `isSheaf_iso_iff`, `toType_isSheaf`, `Alexandrov.isSheaf_principalsKanExtension`, `isSheaf_iff_isSheafEqualizerProducts`, `isSheaf_iff_isTerminal_of_indiscrete`

---

← Back to Index