Documentation Verification Report

Sheaf

📁 Source: Mathlib/Topology/Sheaves/Sheaf.lean

Statistics

Metric	Count
Definitions `Sheaf`, `forget`, `presheaf`, `instCategorySheaf`, `sheafInhabited`	5
Theorems `section_ext`, `isSheaf_iso_iff`, `isSheaf_of_iso`, `isSheaf_unit`, `comp_app`, `forgetFaithful`, `forget_full`, `id_app`	8
Total	13

TopCat

Definitions

Name	Category	Theorems
`Sheaf` 📖	CompOp	33 math math: `Presheaf.mono_of_stalk_mono`, `Sheaf.forgetFaithful`, `Sheaf.pushforward_map`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app`, `Sheaf.id_app`, `Sheaf.instIsLeftAdjointPullback`, `AlgebraicGeometry.tilde.isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `AlgebraicGeometry.tilde.isIso_toOpen_top`, `instHasLimitsOfSizeSheafOfHasLimits`, `Sheaf.comp_app`, `Sheaf.pushforward_obj_val`, `Presheaf.stalkFunctor_preserves_mono`, `Presheaf.isIso_of_stalkFunctor_map_iso`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `Sheaf.forget_full`, `AlgebraicGeometry.tilde.toOpen_res`, `AlgebraicGeometry.tilde.toOpen_res_assoc`, `AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen`, `Sheaf.instIsRightAdjointPushforward`, `instHasLimitsOfShapeSheaf`, `AlgebraicGeometry.tilde.toOpen_map_app_assoc`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app`, `Presheaf.isIso_iff_stalkFunctor_map_iso`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app`, `Presheaf.mono_iff_stalk_mono`, `instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `Sheaf.pushforward_forget`, `AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `AlgebraicGeometry.tilde.toOpen_map_app`
`instCategorySheaf` 📖	CompOp	33 math math: `Presheaf.mono_of_stalk_mono`, `Sheaf.forgetFaithful`, `Sheaf.pushforward_map`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app`, `Sheaf.id_app`, `Sheaf.instIsLeftAdjointPullback`, `AlgebraicGeometry.tilde.isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `AlgebraicGeometry.tilde.isIso_toOpen_top`, `instHasLimitsOfSizeSheafOfHasLimits`, `Sheaf.comp_app`, `Sheaf.pushforward_obj_val`, `Presheaf.stalkFunctor_preserves_mono`, `Presheaf.isIso_of_stalkFunctor_map_iso`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `Sheaf.forget_full`, `AlgebraicGeometry.tilde.toOpen_res`, `AlgebraicGeometry.tilde.toOpen_res_assoc`, `AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen`, `Sheaf.instIsRightAdjointPushforward`, `instHasLimitsOfShapeSheaf`, `AlgebraicGeometry.tilde.toOpen_map_app_assoc`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app`, `Presheaf.isIso_iff_stalkFunctor_map_iso`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app`, `Presheaf.mono_iff_stalk_mono`, `instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `Sheaf.pushforward_forget`, `AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `AlgebraicGeometry.tilde.toOpen_map_app`
`sheafInhabited` 📖	CompOp	—

TopCat.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_iso_iff` 📖	mathematical	—	`IsSheaf`	—	`CategoryTheory.Presheaf.isSheaf_of_iso_iff`
`isSheaf_of_iso` 📖	—	`IsSheaf`	—	—	`isSheaf_iso_iff`
`isSheaf_unit` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Discrete.instSubsingleton`

TopCat.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`section_ext` 📖	—	`TopCat.Presheaf.IsSheaf` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `Opposite.unop` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE`	—	—	`CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Presieve.IsSheaf.isSheafFor` `CategoryTheory.Sieve.le_generate`

TopCat.Sheaf

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	4 math math: `forgetFaithful`, `TopCat.Presheaf.stalkFunctor_preserves_mono`, `forget_full`, `pushforward_forget`
`presheaf` 📖	CompOp	62 math math: `smoothSheafCommRing.ι_forgetStalk_inv`, `instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing`, `smoothSheafCommRing.nonunits_stalk`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv`, `AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk`, `smoothSheafCommRing.ι_evalHom_apply`, `smoothSheafCommRing.eval_germ`, `AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc`, `smoothSheafCommRing.instLocalRing_stalk`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app`, `TopCat.Presheaf.stalkToFiber_injective`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk`, `AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes`, `AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk`, `TopCat.stalkToFiber_germ`, `TopCat.stalkToFiber_injective`, `smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc`, `smoothSheafCommRing.forgetStalk_inv_comp_eval`, `smoothSheafCommRing.forgetStalk_inv_comp_eval_apply`, `smoothSheafCommRing.isUnit_stalk_iff`, `AlgebraicGeometry.tilde.isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `AlgebraicGeometry.germ_comp_stalkToFiberRingHom`, `smoothSheafCommRing.ι_evalHom`, `smoothSheafCommRing.evalHom_germ`, `smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `TopCat.stalkToFiber_surjective`, `AlgebraicGeometry.tilde.isIso_toOpen_top`, `TopCat.Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf`, `smoothSheafCommRing.ι_forgetStalk_inv_apply`, `smoothSheaf.obj_eq`, `smoothSheafCommRing.eval_surjective`, `smoothSheafCommRing.forgetStalk_hom_comp_evalHom`, `AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply`, `smoothSheafCommRing.ι_forgetStalk_inv_assoc`, `smoothSheaf.eval_germ`, `AlgebraicGeometry.Scheme.toOpen_eq`, `instNontrivialStalkPresheafSmoothSheaf`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `smoothSheafCommRing.ι_forgetStalk_hom_apply`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `smoothSheafCommRing.ι_forgetStalk_hom_assoc`, `AlgebraicGeometry.StructureSheaf.stalkAlgebra_map`, `AlgebraicGeometry.tilde.toOpen_res`, `AlgebraicGeometry.tilde.toOpen_res_assoc`, `AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec`, `smoothSheafCommRing.ι_evalHom_assoc`, `smoothSheafCommRing.ι_forgetStalk_hom`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ`, `smoothSheaf.eval_surjective`, `AlgebraicGeometry.tilde.toOpen_map_app_assoc`, `TopCat.Presheaf.stalkToFiber_surjective`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`, `smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply`, `AlgebraicGeometry.Proj.stalkIso'_symm_mk`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom`, `AlgebraicGeometry.tilde.toOpen_map_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.CategoryStruct.comp` `TopCat.Sheaf` `CategoryTheory.Category.toCategoryStruct` `TopCat.instCategorySheaf` `CategoryTheory.Functor.obj`	—	—
`forgetFaithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `TopCat.Sheaf` `TopCat.instCategorySheaf` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `forget`	—	`CategoryTheory.Sheaf.Hom.ext`
`forget_full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `TopCat.Sheaf` `TopCat.instCategorySheaf` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `forget`	—	—
`id_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.CategoryStruct.id` `TopCat.Sheaf` `CategoryTheory.Category.toCategoryStruct` `TopCat.instCategorySheaf` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index