Documentation Verification Report

Functors

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

Statistics

Metric	Count
Definitions `pullback`, `pullbackIso`, `pullbackPushforwardAdjunction`, `pushforward`, `pushforwardForgetIso`	5
Theorems `instIsLeftAdjointPullback`, `instIsRightAdjointPushforward`, `pushforward_forget`, `pushforward_map`, `pushforward_obj_val`, `pushforward_sheaf_of_sheaf`	6
Total	11

TopCat.Sheaf

Definitions

Name	Category	Theorems
`pullback` 📖	CompOp	1 math math: `instIsLeftAdjointPullback`
`pullbackIso` 📖	CompOp	—
`pullbackPushforwardAdjunction` 📖	CompOp	—
`pushforward` 📖	CompOp	6 math math: `pushforward_map`, `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.Sheaf.Hom.val` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology` `CategoryTheory.Functor.obj` `TopCat.Sheaf` `TopCat.instCategorySheaf` `pushforward` `CategoryTheory.Functor.map` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward` `CategoryTheory.Sheaf.val`	—	—
`pushforward_obj_val` 📖	mathematical	—	`CategoryTheory.Sheaf.val` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `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`	`CategoryTheory.Functor.obj` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward`	—	`CategoryTheory.Functor.op_comp_isSheaf` `instIsContinuousOpensCarrierMapGrothendieckTopology`

---

← Back to Index