Documentation Verification Report

LocalPredicate

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

Statistics

Metric	Count
Definitions `LocalPredicate`, `and`, `toPrelocalPredicate`, `PrelocalPredicate`, `and`, `pred`, `sheafify`, `continuousLocal`, `continuousPrelocal`, `inhabitedLocalPredicate`, `inhabitedPrelocalPredicate`, `isSection`, `sheafToTop`, `stalkToFiber`, `subpresheafContinuousPrelocalIsoPresheafToTop`, `subpresheafToTypes`, `subtype`, `subsheafToTypes`	18
Theorems `locality`, `res`, `sheafifyOf`, `sheafify_inductionOn`, `sheafify_inductionOn'`, `sheafify_inductionOn₂`, `sheafify_inductionOn₂'`, `continuousPrelocal_pred`, `stalkToFiber_germ`, `stalkToFiber_injective`, `stalkToFiber_surjective`, `isSheaf`, `subpresheafToTypes_map_coe`, `subpresheafToTypes_obj`, `subsheafToTypes_obj`	15
Total	33

TopCat

Definitions

Name	Category	Theorems
`LocalPredicate` 📖	CompData	—
`PrelocalPredicate` 📖	CompData	—
`continuousLocal` 📖	CompOp	—
`continuousPrelocal` 📖	CompOp	1 math math: `continuousPrelocal_pred`
`inhabitedLocalPredicate` 📖	CompOp	—
`inhabitedPrelocalPredicate` 📖	CompOp	—
`isSection` 📖	CompOp	—
`sheafToTop` 📖	CompOp	—
`stalkToFiber` 📖	CompOp	3 math math: `stalkToFiber_germ`, `stalkToFiber_injective`, `stalkToFiber_surjective`
`subpresheafContinuousPrelocalIsoPresheafToTop` 📖	CompOp	—
`subpresheafToTypes` 📖	CompOp	4 math math: `subpresheafToTypes_map_coe`, `subpresheafToTypes.isSheaf`, `subsheafToTypes_obj`, `subpresheafToTypes_obj`
`subsheafToTypes` 📖	CompOp	4 math math: `stalkToFiber_germ`, `stalkToFiber_injective`, `stalkToFiber_surjective`, `subsheafToTypes_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousPrelocal_pred` 📖	mathematical	—	`PrelocalPredicate.pred` `continuousPrelocal` `Continuous` `carrier` `TopologicalSpace.Opens` `str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	—	—
`stalkToFiber_germ` 📖	mathematical	`carrier` `TopologicalSpace.Opens` `str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`stalkToFiber` `Presheaf.germ` `CategoryTheory.types` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `Sheaf.presheaf` `subsheafToTypes` `PrelocalPredicate.pred` `LocalPredicate.toPrelocalPredicate` `Opposite.unop` `TopologicalSpace.Opens` `carrier` `str` `Opposite.op` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	`CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `CategoryTheory.Limits.Types.Colimit.ι_desc_apply`
`stalkToFiber_injective` 📖	mathematical	`TopologicalSpace.OpenNhds` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `DFunLike.coe` `carrier` `TopologicalSpace.Opens` `str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopologicalSpace.OpenNhds.opensNhds.instFunLike`	`Presheaf.stalk` `CategoryTheory.types` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `Sheaf.presheaf` `subsheafToTypes` `stalkToFiber`	—	`CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.Types.jointly_surjective'` `CategoryTheory.Limits.Types.Colimit.ι_desc_apply` `PrelocalPredicate.res` `CategoryTheory.Limits.Types.colimit_sound`
`stalkToFiber_surjective` 📖	mathematical	`TopologicalSpace.OpenNhds` `PrelocalPredicate.pred` `LocalPredicate.toPrelocalPredicate` `TopologicalSpace.Opens` `carrier` `str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`Presheaf.stalk` `CategoryTheory.types` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `Sheaf.presheaf` `subsheafToTypes` `stalkToFiber`	—	`CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self` `stalkToFiber_germ`
`subpresheafToTypes_map_coe` 📖	mathematical	—	`PrelocalPredicate.pred` `Opposite.unop` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `subpresheafToTypes` `DFunLike.coe` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopologicalSpace.Opens.opensHom.instFunLike` `Quiver.Hom.unop`	—	—
`subpresheafToTypes_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `subpresheafToTypes` `PrelocalPredicate.pred` `Opposite.unop`	—	—
`subsheafToTypes_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `subsheafToTypes` `subpresheafToTypes` `LocalPredicate.toPrelocalPredicate`	—	—

TopCat.LocalPredicate

Definitions

Name	Category	Theorems
`and` 📖	CompOp	—
`toPrelocalPredicate` 📖	CompOp	41 math math: `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply`, `AlgebraicGeometry.Proj.isLocallyFraction_comapStructureSheafFun`, `AlgebraicGeometry.Proj.pow_apply`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem'`, `AlgebraicGeometry.Proj.mul_apply`, `smoothSheafCommRing.eval_germ`, `AlgebraicGeometry.structureSheafInType.mul_apply`, `TopCat.PrelocalPredicate.sheafify_inductionOn`, `AlgebraicGeometry.Proj.one_apply`, `AlgebraicGeometry.Proj.sub_apply`, `AlgebraicGeometry.StructureSheaf.comap_apply`, `TopCat.stalkToFiber_germ`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem'`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem'`, `smoothSheafCommRing.evalHom_germ`, `AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply`, `TopCat.PrelocalPredicate.sheafify_inductionOn'`, `StructureGroupoid.LocalInvariantProp.section_spec`, `AlgebraicGeometry.StructureSheaf.isLocallyFraction_comapFun`, `AlgebraicGeometry.Proj.zero_apply`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem'`, `AlgebraicGeometry.structureSheafInType.add_apply`, `AlgebraicGeometry.Proj.ext_iff`, `TopCat.subpresheafToTypes.isSheaf`, `TopCat.subsheafToTypes_obj`, `smoothSheaf.eval_germ`, `AlgebraicGeometry.Proj.add_apply`, `AlgebraicGeometry.StructureSheaf.res_apply`, `TopCat.PrelocalPredicate.sheafifyOf`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `locality`, `smoothSheaf.contMDiff_section`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem'`, `AlgebraicGeometry.Proj.res_apply`, `AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom`, `AlgebraicGeometry.StructureSheaf.const_apply`, `AlgebraicGeometry.structureSheafInType.smul_apply`, `TopCat.PrelocalPredicate.sheafify_inductionOn₂`, `TopCat.PrelocalPredicate.sheafify_inductionOn₂'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locality` 📖	mathematical	`TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.PrelocalPredicate.pred` `toPrelocalPredicate` `DFunLike.coe` `TopologicalSpace.Opens.opensHom.instFunLike`	`TopCat.PrelocalPredicate.pred` `toPrelocalPredicate`	—	—

TopCat.PrelocalPredicate

Definitions

Name	Category	Theorems
`and` 📖	CompOp	—
`pred` 📖	MathDef	43 math math: `res`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply`, `AlgebraicGeometry.Proj.isLocallyFraction_comapStructureSheafFun`, `AlgebraicGeometry.Proj.pow_apply`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem'`, `AlgebraicGeometry.Proj.mul_apply`, `smoothSheafCommRing.eval_germ`, `AlgebraicGeometry.structureSheafInType.mul_apply`, `sheafify_inductionOn`, `AlgebraicGeometry.Proj.one_apply`, `AlgebraicGeometry.Proj.sub_apply`, `AlgebraicGeometry.StructureSheaf.comap_apply`, `TopCat.stalkToFiber_germ`, `TopCat.continuousPrelocal_pred`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem'`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem'`, `smoothSheafCommRing.evalHom_germ`, `AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply`, `sheafify_inductionOn'`, `StructureGroupoid.LocalInvariantProp.section_spec`, `AlgebraicGeometry.StructureSheaf.isLocallyFraction_comapFun`, `AlgebraicGeometry.Proj.zero_apply`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem'`, `TopCat.subpresheafToTypes_map_coe`, `AlgebraicGeometry.structureSheafInType.add_apply`, `AlgebraicGeometry.Proj.ext_iff`, `smoothSheaf.eval_germ`, `AlgebraicGeometry.Proj.add_apply`, `AlgebraicGeometry.StructureSheaf.res_apply`, `sheafifyOf`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `TopCat.LocalPredicate.locality`, `smoothSheaf.contMDiff_section`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem'`, `AlgebraicGeometry.Proj.res_apply`, `AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom`, `AlgebraicGeometry.StructureSheaf.const_apply`, `TopCat.subpresheafToTypes_obj`, `AlgebraicGeometry.structureSheafInType.smul_apply`, `sheafify_inductionOn₂`, `sheafify_inductionOn₂'`
`sheafify` 📖	CompOp	5 math math: `sheafify_inductionOn`, `sheafify_inductionOn'`, `sheafifyOf`, `sheafify_inductionOn₂`, `sheafify_inductionOn₂'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`res` 📖	mathematical	`pred`	`pred` `DFunLike.coe` `Quiver.Hom` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopologicalSpace.Opens.opensHom.instFunLike`	—	—
`sheafifyOf` 📖	mathematical	`pred`	`pred` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify`	—	—
`sheafify_inductionOn` 📖	mathematical	`TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `pred` `DFunLike.coe` `TopologicalSpace.Opens.opensHom.instFunLike` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify`	`pred` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	—
`sheafify_inductionOn'` 📖	mathematical	`pred` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify`	`pred` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	`sheafify_inductionOn`
`sheafify_inductionOn₂` 📖	mathematical	`TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `pred` `DFunLike.coe` `TopologicalSpace.Opens.opensHom.instFunLike` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify`	`pred` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	—
`sheafify_inductionOn₂'` 📖	mathematical	`pred` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Set` `Set.instMembership` `SetLike.coe` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify`	`pred` `TopCat.LocalPredicate.toPrelocalPredicate` `sheafify` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	`sheafify_inductionOn₂`

TopCat.subpresheafToTypes

Definitions

Name	Category	Theorems
`subtype` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf` 📖	mathematical	—	`TopCat.Presheaf.IsSheaf` `CategoryTheory.types` `TopCat.subpresheafToTypes` `TopCat.LocalPredicate.toPrelocalPredicate`	—	`TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types` `TopCat.Sheaf.existsUnique_gluing` `CategoryTheory.Limits.Types.hasLimitsOfSize` `univLE_of_max` `UnivLE.self` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `TopCat.LocalPredicate.locality` `TopologicalSpace.Opens.mem_iSup`

---

← Back to Index