Structures · Category theory
CategoryTheory.Precoverage.ZeroHypercover.Small
A w-0-hypercover E is w'-small if there exists an indexing type ι in Type w' and a
restriction map ι → E.I₀ such that the restriction of E to ι is still covering.
Note: This is weaker than E.I₀ being w'-small. For example, every Zariski cover of
X : Scheme.{u} is u-small, because X itself suffices as indexing type.
- Shape
- One type argument · adds exists_restrictIndex_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun
- CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall
- CategoryTheory.Precoverage.ZeroHypercover.Small.Index
- CategoryTheory.MorphismProperty.of_zeroHypercover_target
- CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover
- CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem
- CategoryTheory.MorphismProperty.of_zeroHypercover_source
- CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁
- CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall.congr_simp
- CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀
Ancestors0
No ancestors.