Documentation Verification Report

Functors

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

Statistics

Metric	Count
Definitions `pullback`, `pullbackIso`, `pullbackPushforwardAdjunction`, `pushforward`, `pushforwardForgetIso`, `sheafPullback`, `sheafPullbackIso`	7
Theorems `instIsLeftAdjointPullback`, `instIsRightAdjointPushforward`, `pushforward_forget`, `pushforward_map`, `pushforward_obj_val`, `pushforward_sheaf_of_sheaf`	6
Total	13

TopCat.Sheaf

Definitions

Name	Category	Theorems
`pullback` 📖	CompOp	1 math math: `instIsLeftAdjointPullback`
`pullbackIso` 📖	CompOp	—
`pullbackPushforwardAdjunction` 📖	CompOp	—
`pushforward` 📖	CompOp	7 math math: `pushforward_map`, `IsFlasque.pushforward_isFlasque`, `pushforward_obj_val`, `instIsRightAdjointPushforward`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app`, `pushforward_forget`
`pushforwardForgetIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLeftAdjointPullback` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `TopCat.Sheaf` `TopCat.instCategorySheaf` `pullback`	—	`CategoryTheory.Adjunction.isLeftAdjoint`
`instIsRightAdjointPushforward` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `TopCat.Sheaf` `TopCat.instCategorySheaf` `pushforward`	—	`CategoryTheory.Adjunction.isRightAdjoint`
`pushforward_forget` 📖	mathematical	—	`CategoryTheory.Functor.comp` `TopCat.Sheaf` `TopCat.instCategorySheaf` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `pushforward` `forget` `TopCat.Presheaf.pushforward`	—	—
`pushforward_map` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `TopCat.Sheaf` `TopCat.instCategorySheaf` `pushforward` `CategoryTheory.Functor.map` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward`	—	—
`pushforward_obj_val` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `CategoryTheory.Functor.obj` `TopCat.Sheaf` `TopCat.instCategorySheaf` `pushforward` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward`	—	—
`pushforward_sheaf_of_sheaf` 📖	mathematical	`TopCat.Presheaf.IsSheaf`	`TopCat.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward`	—	`CategoryTheory.Functor.op_comp_isSheaf` `instIsContinuousOpensCarrierMapGrothendieckTopology`

Topology.IsOpenEmbedding

Definitions

Name	Category	Theorems
`sheafPullback` 📖	CompOp	—
`sheafPullbackIso` 📖	CompOp	—

---

← Back to Index