Structures · Category theory
CategoryTheory.ObjectProperty.EssentiallySmall
A property of objects is essentially small relative to a universe w
if it is contained in the closure by isomorphisms of a small property.
- Shape
- One type argument · adds exists_small_le'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances3
- CategoryTheory.Comma
- CategoryTheory.CardinalDirectedPoset
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
- CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le'
- CategoryTheory.ObjectProperty.EssentiallySmall.of_le
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι
- CommRingCat.essentiallySmall_of_localizationAway
- CommRingCat.essentiallySmall_of_finiteType
- CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top
- CategoryTheory.ObjectProperty.instEssentiallySmallMax
- CategoryTheory.ObjectProperty.instEssentiallySmallUnopOfOpposite
- CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall
- CategoryTheory.ObjectProperty.instEssentiallySmallISupOfSmall
- CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator
- CategoryTheory.ObjectProperty.instEssentiallySmallCommaCommaOfLocallySmall
- CategoryTheory.ObjectProperty.instEssentiallySmallLimitsClosureOfSmallOfLocallySmall
- CategoryTheory.ObjectProperty.instEssentiallySmallColimitsClosureOfSmallOfLocallySmall
- CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall
- CategoryTheory.ObjectProperty.EssentiallySmall.exists_small
- CategoryTheory.ObjectProperty.isEssentiallySmall_limitsClosure
- CategoryTheory.ObjectProperty.instEssentiallySmallOppositeOp
- CategoryTheory.ObjectProperty.instEssentiallySmallRetractClosureOfLocallySmall
- CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable
- CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1
- CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty
- CategoryTheory.ObjectProperty.instEssentiallySmallMap
- CategoryTheory.ObjectProperty.instEssentiallySmallIsoClosure
Ancestors0
No ancestors.