Structures · Category theory
CategoryTheory.WellPowered
A category (with morphisms in Type v) is well-powered relative to a universe w
if it is locally small and Subobject X is w-small for every X.
We show in wellPowered_of_essentiallySmall_monoOver and essentiallySmall_monoOver
that this is the case if and only if MonoOver X is w-essentially small for every X.
- Shape
- One type argument · adds subobject_small
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- ModuleCat
- AddCommGrpCat
- CategoryTheory.ShrinkHoms
- PresheafOfModules
- CategoryTheory.StructuredArrow
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- CategoryTheory.Subobject.wideCospan
- CategoryTheory.Subobject.widePullbackι
- CategoryTheory.Subobject.sSup
- CategoryTheory.Subobject.smallCoproductDesc
- CategoryTheory.Subobject.widePullback
- CategoryTheory.hasInitial_of_isCoseparating
- CategoryTheory.Subobject.sInf
- CategoryTheory.Subobject.leInfCone
- CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating
- CategoryTheory.Subobject.leInfCone_π_app_none
- CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating
- CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating
- CategoryTheory.wellPowered_of_equiv
- CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating
- CategoryTheory.hasTerminal_of_isSeparating
- CategoryTheory.instWellPoweredShrinkHoms
- CategoryTheory.Subobject.instCompleteLattice
- CategoryTheory.Subobject.wideCospan_map_term
- CategoryTheory.Subobject.completeSemilatticeInf
- CategoryTheory.Abelian.wellPowered_opposite
- CategoryTheory.essentiallySmall_monoOver
- CategoryTheory.Subobject.widePullbackι_mono
- CategoryTheory.Subobject.sSup_le
- CategoryTheory.Subobject.sInf_le
- CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator
- CategoryTheory.Subobject.le_sSup
- CategoryTheory.small_subobject
- CategoryTheory.Subobject.completeSemilatticeSup
- CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator
- CategoryTheory.WellPowered.subobject_small
- CategoryTheory.Subobject.le_sInf
- CategoryTheory.CostructuredArrow.well_copowered_costructuredArrow
- CategoryTheory.StructuredArrow.wellPowered_structuredArrow
Ancestors0
No ancestors.