Structures · Category theory
CategoryTheory.Precoverage.Small
A precoverage is w-small, if every 0-hypercover is w-small.
- Shape
- One type argument · adds zeroHypercoverSmall
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- AlgebraicGeometry.Scheme
- TopCat
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_small
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small
- CategoryTheory.Precoverage.instSmallComap
- CategoryTheory.Precoverage.Small.zeroHypercoverSmall
- CategoryTheory.Precoverage.instSmallOfSmall
- CategoryTheory.Precoverage.Small.inf
- CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small
Ancestors0
No ancestors.