Structures · Category theory
CategoryTheory.Limits.HasFiniteColimits
A category has all finite colimits if every functor J ⥤ C with a FinCategory J
instance and J : Type has a colimit.
This is often called 'finitely cocomplete'.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances18
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- HomologicalComplex
- Action
- CategoryTheory.Comma
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.CostructuredArrow
- CategoryTheory.Arrow
- CategoryTheory.ShortComplex
- FGModuleCat
- FintypeCat
- CochainComplex.Plus
- CategoryTheory.MorphismProperty.Under
- Condensed
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by68
- CategoryTheory.CostructuredArrow.projectQuotient
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux
- CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op
- CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
- CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
- CategoryTheory.hasExactLimitsOfShape_of_initial
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom
- CategoryTheory.coflat_of_preservesFiniteColimits
- CategoryTheory.HasExactLimitsOfShape.domain_of_functor
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
- Action.instPreservesFiniteColimitsForgetOfHasFiniteColimits
- instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology
- Action.instHasFiniteColimits
- HomologicalComplex.instEpiFOfHasFiniteColimits
- CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits
- CategoryTheory.Ind.leftExactFunctorEquivalence
- CategoryTheory.CostructuredArrow.lift_projectQuotient
- CategoryTheory.CostructuredArrow.projectQuotient_mk
- Condensed.hasExactLimitsOfShape
- HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits
- CategoryTheory.instHasFiniteBiproductsInd
- CategoryTheory.preservesFiniteColimits_iff_coflat
- CochainComplex.Plus.instHasFiniteColimits
- CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃
- CategoryTheory.Limits.has_colimits_of_finite_and_filtered
- CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits
- CategoryTheory.Arrow.hasFiniteColimits
- CategoryTheory.CostructuredArrow.projectQuotient_factors
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat
- CategoryTheory.Limits.instHasFiniteColimitsFunctor
- CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf
- Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits
- CategoryTheory.Limits.preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits
- CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms
- CategoryTheory.Ind.isSeparator_range_yoneda
- CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits
- CategoryTheory.CountableAB4Star.of_countableAB5Star
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post
- CategoryTheory.Limits.hasFiniteColimits_of_hasColimits_of_createsFiniteColimits
- CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
- CategoryTheory.AB4Star.of_AB5Star
- CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits
- CategoryTheory.IsFiltered.of_hasFiniteColimits
- CategoryTheory.Over.instHasFiniteColimits
- CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits
- CategoryTheory.ShortComplex.hasFiniteColimits
- HomotopicalAlgebra.ModelCategory.mk'
- CategoryTheory.Comma.hasFiniteColimits
Ancestors0
No ancestors.