Structures · Category theory
CategoryTheory.Limits.HasColimitsOfSize
C has all colimits of size v₁ u₁ (HasColimitsOfSize.{v₁ u₁} C)
if it has colimits of every shape J : Type u₁ with [Category.{v₁} J].
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Shape
- One type argument · adds has_colimits_of_shape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances17
- CategoryTheory.Functor
- CategoryTheory.Discrete
- ModuleCat
- AddCommGrpCat
- TopCat
- SheafOfModules
- CategoryTheory.Skeleton
- CategoryTheory.Comma
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.CostructuredArrow
- TopCat.Presheaf
- CategoryTheory.Subobject
- CategoryTheory.ThinSkeleton
- CategoryTheory.MonoOver
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by208
- CategoryTheory.GrothendieckTopology.Point.presheafFiber
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv
- CategoryTheory.GrothendieckTopology.Point.sheafFiber
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap
- CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc
- CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc
- CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext
- CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm
- CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_apply
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w
- CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality
- CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_app
- CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η
- CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulConstantSheaf
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π
- CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom
- CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone
- CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape
- CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality
- CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall
- CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone
- CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_assoc
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso
- CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp
- CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc.congr_simp
- CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone
- CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ
- CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_id
Ancestors0
No ancestors.