Documentation Verification Report

Comap

📁 Source: Mathlib/CategoryTheory/Sites/Point/Comap.lean

Statistics

Metric	Count
Definitions `comap`, `sheafFiberComapIso`, `skyscraperSheafFunctorCompSheafPushforwardContinuous`	3
Theorems `comap_fiber`, `sheafFiberComapIso_hom_app`, `sheafFiberComapIso_inv_app`	3
Total	6

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	3 math math: `comap_fiber`, `sheafFiberComapIso_hom_app`, `sheafFiberComapIso_inv_app`
`sheafFiberComapIso` 📖	CompOp	2 math math: `sheafFiberComapIso_hom_app`, `sheafFiberComapIso_inv_app`
`skyscraperSheafFunctorCompSheafPushforwardContinuous` 📖	CompOp	2 math math: `sheafFiberComapIso_hom_app`, `sheafFiberComapIso_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_fiber` 📖	mathematical	`CategoryTheory.CoverPreserving`	`fiber` `comap` `CategoryTheory.Functor.comp` `CategoryTheory.types`	—	—
`sheafFiberComapIso_hom_app` 📖	mathematical	`CategoryTheory.CoverPreserving` `CategoryTheory.Limits.HasProducts`	`CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `sheafFiber` `comap` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sheafPullback` `CategoryTheory.Iso.hom` `sheafFiberComapIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.sheafPushforwardContinuous` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.sheafAdjunctionContinuous` `skyscraperSheafFunctor` `skyscraperSheafAdjunction` `skyscraperSheafFunctorCompSheafPushforwardContinuous` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Adjunction.comp_unit_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc`
`sheafFiberComapIso_inv_app` 📖	mathematical	`CategoryTheory.CoverPreserving` `CategoryTheory.Limits.HasProducts`	`CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sheafPullback` `sheafFiber` `comap` `CategoryTheory.Iso.inv` `sheafFiberComapIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `skyscraperSheafFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `skyscraperSheafAdjunction` `CategoryTheory.Functor.sheafPushforwardContinuous` `skyscraperSheafFunctorCompSheafPushforwardContinuous` `CategoryTheory.Adjunction.counit` `CategoryTheory.Functor.sheafAdjunctionContinuous`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Adjunction.comp_counit_app`

---

← Back to Index