Structures · Category theory
CategoryTheory.EssentiallySmall
A category is EssentiallySmall.{w} if there exists
an equivalence to some S : Type w with [SmallCategory S].
- Defined in
- Mathlib.CategoryTheory.EssentiallySmall
- Shape
- One type argument · adds equiv_smallCategory
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances11
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- AlgebraicGeometry.Scheme.AffineEtale
- LightDiagram
- CategoryTheory.Functor.Elements
- FGModuleCat
- LightProfinite
- CategoryTheory.MonoOver
- FGAlgCat
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- CategoryTheory.equivSmallModel
- CategoryTheory.SmallModel
- CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
- CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall
- CategoryTheory.finallySmall_of_essentiallySmall
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit'
- CategoryTheory.essentiallySmall_of_fully_faithful
- CategoryTheory.hasSheafifyEssentiallySmallSite
- CategoryTheory.MorphismProperty.isClosedUnderColimitsOfShape_isLocal
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense
- CategoryTheory.initiallySmall_of_essentiallySmall
- CategoryTheory.ObjectProperty.of_essentiallySmall_index
- CategoryTheory.EssentiallySmall.equiv_smallCategory
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit
- CategoryTheory.initiallySmall_of_initial_of_essentiallySmall
- CategoryTheory.finallySmall_of_final_of_essentiallySmall
- CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall
- CategoryTheory.SmallModel.congr_simp
- CategoryTheory.instLocallySmallSmallModel
- CategoryTheory.CostructuredArrow.essentiallySmall
- CategoryTheory.small_skeleton_of_essentiallySmall
- CategoryTheory.instEssentiallySmallOpposite
- CategoryTheory.Limits.hasLimitsOfShape_of_essentiallySmall
- CategoryTheory.Equivalence.instPrecoherentSmallModel
- CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall
- CategoryTheory.instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall
- CategoryTheory.smallSheafify
- CategoryTheory.Equivalence.instPreregularSmallModel
- CategoryTheory.smallSheafificationAdjunction
- CategoryTheory.hasLimitsEssentiallySmallSite
- CategoryTheory.ObjectProperty.instEssentiallySmallTopOfEssentiallySmall
- CategoryTheory.instMonoidalClosedFunctorTypeOfEssentiallySmall
- CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow
- CategoryTheory.locallySmall_of_essentiallySmall
- CategoryTheory.smallCategorySmallModel
- CategoryTheory.Limits.hasColimitsOfShape_of_essentiallySmall
- CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall
- CategoryTheory.Limits.HasColimitsOfShape.of_essentiallySmall
- CategoryTheory.Functor.Elements.essentiallySmall
- CategoryTheory.GrothendieckTopology.instPreservesSheafification_1
- CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall
- CategoryTheory.hasSheafComposeEssentiallySmallSite
- CategoryTheory.Limits.HasLimitsOfShape.of_essentiallySmall
- CategoryTheory.ObjectProperty.instEssentiallySmallEssImageOfEssentiallySmall
- CategoryTheory.hasColimitsEssentiallySmallSite
- CategoryTheory.StructuredArrow.essentiallySmall
- CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall
- CategoryTheory.Sheaf.instHasSubobjectClassifierTypeOfEssentiallySmall
Ancestors0
No ancestors.