Theorems · Definition · category theory
TopCat.Presheaf
(C : Type u) → [CategoryTheory.Category.{v, u} C] → TopCat → Type (max u v w)The category of C-valued presheaves on a (bundled) topological space X.
- Defined in
- Mathlib.Topology.Sheaves.Presheaf
- Cited by
- 371 results in Mathlib
- Foundations
- Depth 25 from the axioms, rests on 148 definitions · uses propext, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorproof · cited by 16,252
- Oppositeproof · cited by 8,081
- TopCat.carrierproof · cited by 3,184
- TopologicalSpace.Opensproof · cited by 2,040
- TopCatstatement and proof · cited by 1,889
Cited by526
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.PresheafedSpace.presheafstatement · cited by 1,104
- TopCat.Presheaf.stalkstatement and proof · cited by 407
- TopCat.Presheaf.germstatement and proof · cited by 208
- TopCat.Presheaf.pushforwardstatement · cited by 174
- AlgebraicGeometry.PresheafedSpace.Hom.cstatement · cited by 142
- TopCat.Sheaf.presheafstatement · cited by 79
- AlgebraicGeometry.Scheme.Modules.presheafstatement · cited by 59
- TopCat.Presheaf.stalkSpecializesstatement and proof · cited by 51
- TopCat.Presheaf.IsSheafstatement and proof · cited by 38
- TopCat.Presheaf.stalkFunctorstatement · cited by 37
- TopCat.Presheaf.restrictOpenstatement and proof · cited by 25
- TopCat.Presheaf.stalkCongrstatement and proof · cited by 23
Showing the 200 most cited of 526.