Documentation Verification Report

Skyscraper

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

Statistics

Metric	Count
Definitions `map'`, `counit`, `fromStalk`, `toSkyscraperPresheaf`, `unit`, `skyscraperPresheaf`, `skyscraperPresheafCocone`, `skyscraperPresheafCoconeIsColimitOfNotSpecializes`, `skyscraperPresheafCoconeIsColimitOfSpecializes`, `skyscraperPresheafCoconeOfSpecializes`, `skyscraperPresheafFunctor`, `skyscraperPresheafStalkAdjunction`, `skyscraperPresheafStalkOfNotSpecializes`, `skyscraperPresheafStalkOfNotSpecializesIsTerminal`, `skyscraperPresheafStalkOfSpecializes`, `skyscraperSheaf`, `skyscraperSheafFunctor`, `stalkSkyscraperSheafAdjunction`	18
Theorems `map'_app`, `map'_comp`, `map'_id`, `counit_app`, `fromStalk_to_skyscraper`, `germ_fromStalk`, `germ_fromStalk_assoc`, `toSkyscraperPresheaf_app`, `to_skyscraper_fromStalk`, `unit_app`, `germ_skyscraperPresheafStalkOfSpecializes_hom`, `germ_skyscraperPresheafStalkOfSpecializes_hom_assoc`, `instIsLeftAdjointPresheafStalkFunctor`, `instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits`, `instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits`, `skyscraperPresheafCoconeOfSpecializes_pt`, `skyscraperPresheafCoconeOfSpecializes_ι_app`, `skyscraperPresheafCocone_pt`, `skyscraperPresheafCocone_ι_app`, `skyscraperPresheafFunctor_map`, `skyscraperPresheafFunctor_obj`, `skyscraperPresheaf_eq_pushforward`, `skyscraperPresheaf_isSheaf`, `skyscraperPresheaf_map`, `skyscraperPresheaf_obj`	25
Total	43

SkyscraperPresheafFunctor

Definitions

Name	Category	Theorems
`map'` 📖	CompOp	4 math math: `map'_comp`, `map'_app`, `skyscraperPresheafFunctor_map`, `map'_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map'_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `map'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `CategoryTheory.Limits.IsTerminal.from` `CategoryTheory.Limits.terminal` `CategoryTheory.Limits.IsTerminal` `CategoryTheory.Limits.terminalIsTerminal`	—	—
`map'_comp` 📖	mathematical	—	`map'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheaf`	—	`TopCat.Presheaf.ext` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.IsTerminal.comp_from`
`map'_id` 📖	mathematical	—	`map'` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheaf`	—	`TopCat.Presheaf.ext` `CategoryTheory.eqToHom_naturality` `CategoryTheory.Category.comp_id` `CategoryTheory.eqToHom_trans` `CategoryTheory.Limits.IsTerminal.from_self`

StalkSkyscraperPresheafAdjunctionAuxs

Definitions

Name	Category	Theorems
`counit` 📖	CompOp	1 math math: `counit_app`
`fromStalk` 📖	CompOp	4 math math: `germ_fromStalk`, `to_skyscraper_fromStalk`, `germ_fromStalk_assoc`, `fromStalk_to_skyscraper`
`toSkyscraperPresheaf` 📖	CompOp	4 math math: `to_skyscraper_fromStalk`, `unit_app`, `fromStalk_to_skyscraper`, `toSkyscraperPresheaf_app`
`unit` 📖	CompOp	1 math math: `unit_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counit_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheafFunctor` `TopCat.Presheaf.stalkFunctor` `CategoryTheory.Functor.id` `counit` `CategoryTheory.Iso.hom` `TopCat.Presheaf.stalk` `skyscraperPresheaf` `skyscraperPresheafStalkOfSpecializes`	—	—
`fromStalk_to_skyscraper` 📖	mathematical	—	`fromStalk` `toSkyscraperPresheaf`	—	`TopCat.Presheaf.stalk_hom_ext` `germ_fromStalk` `toSkyscraperPresheaf_app` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans` `CategoryTheory.eqToHom_refl` `CategoryTheory.Category.comp_id` `TopCat.Presheaf.germ.eq_1`
`germ_fromStalk` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `TopCat.Presheaf.stalk` `TopCat.Presheaf.germ` `fromStalk` `skyscraperPresheaf` `CategoryTheory.NatTrans.app` `CategoryTheory.eqToHom` `Opposite.unop` `CategoryTheory.Limits.terminal`	—	`CategoryTheory.Limits.colimit.ι_desc`
`germ_fromStalk_assoc` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `TopCat.Presheaf.stalk` `TopCat.Presheaf.germ` `fromStalk` `skyscraperPresheaf` `CategoryTheory.NatTrans.app` `CategoryTheory.eqToHom` `Opposite.unop` `CategoryTheory.Limits.terminal`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `germ_fromStalk`
`toSkyscraperPresheaf_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `toSkyscraperPresheaf` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `CategoryTheory.CategoryStruct.comp` `TopCat.Presheaf.stalk` `TopCat.Presheaf.germ` `CategoryTheory.eqToHom` `CategoryTheory.Limits.IsTerminal.from` `CategoryTheory.Limits.terminal` `CategoryTheory.Limits.IsTerminal` `CategoryTheory.Limits.terminalIsTerminal`	—	—
`to_skyscraper_fromStalk` 📖	mathematical	—	`toSkyscraperPresheaf` `fromStalk`	—	`CategoryTheory.NatTrans.ext` `CategoryTheory.Category.assoc` `germ_fromStalk` `CategoryTheory.eqToHom_trans` `CategoryTheory.eqToHom_refl` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsTerminal.hom_ext`
`unit_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `TopCat.Presheaf.stalkFunctor` `skyscraperPresheafFunctor` `unit` `toSkyscraperPresheaf` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `TopCat.Presheaf.stalk`	—	—

(root)

Definitions

Name	Category	Theorems
`skyscraperPresheaf` 📖	CompOp	18 math math: `skyscraperPresheaf_obj`, `StalkSkyscraperPresheafAdjunctionAuxs.counit_app`, `skyscraperPresheafCocone_pt`, `StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk`, `skyscraperPresheafFunctor_obj`, `SkyscraperPresheafFunctor.map'_comp`, `StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc`, `skyscraperPresheafCocone_ι_app`, `skyscraperPresheaf_eq_pushforward`, `germ_skyscraperPresheafStalkOfSpecializes_hom_assoc`, `skyscraperPresheaf_isSheaf`, `skyscraperPresheafCoconeOfSpecializes_ι_app`, `skyscraperPresheafCoconeOfSpecializes_pt`, `SkyscraperPresheafFunctor.map'_app`, `germ_skyscraperPresheafStalkOfSpecializes_hom`, `skyscraperPresheaf_map`, `SkyscraperPresheafFunctor.map'_id`, `StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app`
`skyscraperPresheafCocone` 📖	CompOp	2 math math: `skyscraperPresheafCocone_pt`, `skyscraperPresheafCocone_ι_app`
`skyscraperPresheafCoconeIsColimitOfNotSpecializes` 📖	CompOp	—
`skyscraperPresheafCoconeIsColimitOfSpecializes` 📖	CompOp	—
`skyscraperPresheafCoconeOfSpecializes` 📖	CompOp	2 math math: `skyscraperPresheafCoconeOfSpecializes_ι_app`, `skyscraperPresheafCoconeOfSpecializes_pt`
`skyscraperPresheafFunctor` 📖	CompOp	5 math math: `StalkSkyscraperPresheafAdjunctionAuxs.counit_app`, `skyscraperPresheafFunctor_obj`, `StalkSkyscraperPresheafAdjunctionAuxs.unit_app`, `skyscraperPresheafFunctor_map`, `instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits`
`skyscraperPresheafStalkAdjunction` 📖	CompOp	—
`skyscraperPresheafStalkOfNotSpecializes` 📖	CompOp	—
`skyscraperPresheafStalkOfNotSpecializesIsTerminal` 📖	CompOp	—
`skyscraperPresheafStalkOfSpecializes` 📖	CompOp	3 math math: `StalkSkyscraperPresheafAdjunctionAuxs.counit_app`, `germ_skyscraperPresheafStalkOfSpecializes_hom_assoc`, `germ_skyscraperPresheafStalkOfSpecializes_hom`
`skyscraperSheaf` 📖	CompOp	—
`skyscraperSheafFunctor` 📖	CompOp	1 math math: `instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits`
`stalkSkyscraperSheafAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`germ_skyscraperPresheafStalkOfSpecializes_hom` 📖	mathematical	`Specializes` `TopCat.carrier` `TopCat.str` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `Opposite.op` `TopCat.Presheaf.stalk` `TopCat.Presheaf.germ` `CategoryTheory.Iso.hom` `skyscraperPresheafStalkOfSpecializes` `CategoryTheory.eqToHom` `Set` `Set.instMembership` `TopologicalSpace.Opens.carrier` `Opposite.unop` `CategoryTheory.Limits.terminal` `Specializes.mem_open` `TopologicalSpace.Opens.is_open'`	—	`CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom`
`germ_skyscraperPresheafStalkOfSpecializes_hom_assoc` 📖	mathematical	`Specializes` `TopCat.carrier` `TopCat.str` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `Opposite.op` `TopCat.Presheaf.stalk` `TopCat.Presheaf.germ` `CategoryTheory.Iso.hom` `skyscraperPresheafStalkOfSpecializes` `CategoryTheory.eqToHom` `Set` `Set.instMembership` `TopologicalSpace.Opens.carrier` `CategoryTheory.Limits.terminal` `Opposite.unop` `Specializes.mem_open` `TopologicalSpace.Opens.is_open'`	—	`Specializes.mem_open` `TopologicalSpace.Opens.is_open'` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `germ_skyscraperPresheafStalkOfSpecializes_hom`
`instIsLeftAdjointPresheafStalkFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.stalkFunctor`	—	`CategoryTheory.Adjunction.isLeftAdjoint`
`instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheafFunctor`	—	`CategoryTheory.Adjunction.isRightAdjoint`
`instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `TopCat.Sheaf` `TopCat.instCategorySheaf` `skyscraperSheafFunctor`	—	`CategoryTheory.Adjunction.isRightAdjoint`
`skyscraperPresheafCoconeOfSpecializes_pt` 📖	mathematical	`Specializes` `TopCat.carrier` `TopCat.str`	`CategoryTheory.Limits.Cocone.pt` `Opposite` `TopologicalSpace.OpenNhds` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `CategoryTheory.Functor.comp` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.op` `TopologicalSpace.OpenNhds.inclusion` `skyscraperPresheaf` `skyscraperPresheafCoconeOfSpecializes`	—	—
`skyscraperPresheafCoconeOfSpecializes_ι_app` 📖	mathematical	`Specializes` `TopCat.carrier` `TopCat.str`	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.OpenNhds` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `CategoryTheory.Functor.comp` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.op` `TopologicalSpace.OpenNhds.inclusion` `skyscraperPresheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `skyscraperPresheafCoconeOfSpecializes` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`skyscraperPresheafCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `Opposite` `TopologicalSpace.OpenNhds` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `CategoryTheory.Functor.comp` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.op` `TopologicalSpace.OpenNhds.inclusion` `skyscraperPresheaf` `skyscraperPresheafCocone` `CategoryTheory.Limits.terminal`	—	—
`skyscraperPresheafCocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `TopologicalSpace.OpenNhds` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `CategoryTheory.Functor.comp` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.op` `TopologicalSpace.OpenNhds.inclusion` `skyscraperPresheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.terminal` `CategoryTheory.Limits.Cocone.ι` `skyscraperPresheafCocone` `CategoryTheory.Limits.terminal.from`	—	—
`skyscraperPresheafFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheafFunctor` `SkyscraperPresheafFunctor.map'`	—	—
`skyscraperPresheafFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `skyscraperPresheafFunctor` `skyscraperPresheaf`	—	—
`skyscraperPresheaf_eq_pushforward` 📖	mathematical	—	`skyscraperPresheaf` `CategoryTheory.Functor.obj` `TopCat.Presheaf` `TopCat.of` `TopCat.carrier` `instTopologicalSpacePUnit` `TopCat.instCategoryPresheaf` `TopCat.str` `TopCat.Presheaf.pushforward` `TopCat.ofHom` `ContinuousMap.const`	—	—
`skyscraperPresheaf_isSheaf` 📖	mathematical	—	`TopCat.Presheaf.IsSheaf` `skyscraperPresheaf`	—	`TopCat.Presheaf.isSheaf_iso_iff` `skyscraperPresheaf_eq_pushforward` `TopCat.Sheaf.pushforward_sheaf_of_sheaf` `TopCat.Presheaf.isSheaf_on_punit_of_isTerminal` `Set.notMem_empty`
`skyscraperPresheaf_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `CategoryTheory.Limits.terminal` `CategoryTheory.eqToHom` `CategoryTheory.Limits.IsTerminal.from` `CategoryTheory.Limits.IsTerminal` `CategoryTheory.Limits.terminalIsTerminal`	—	—
`skyscraperPresheaf_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `skyscraperPresheaf` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `CategoryTheory.Limits.terminal`	—	—

---

← Back to Index