Theorems · Inductive type · algebraic geometry
AlgebraicGeometry.PresheafedSpace
(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max (max (u + 1) u_1) v_1)A PresheafedSpace C is a topological space equipped with a presheaf of Cs.
- Cited by
- 260 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by352
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
- AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement · cited by 1,988
- AlgebraicGeometry.PresheafedSpace.Hom.basestatement and proof · cited by 1,135
- AlgebraicGeometry.PresheafedSpace.presheafstatement and proof · cited by 1,104
- AlgebraicGeometry.PresheafedSpace.Hom.cstatement and proof · cited by 142
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersionstatement · cited by 44
- AlgebraicGeometry.PresheafedSpace.Hom.stalkMapstatement and proof · cited by 40
- AlgebraicGeometry.PresheafedSpace.Homstatement · cited by 32
- AlgebraicGeometry.PresheafedSpace.restrictstatement and proof · cited by 31
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctorstatement and proof · cited by 30
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_openstatement and proof · cited by 24
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invAppstatement and proof · cited by 24
Showing the 200 most cited of 352.