Structures · Category theory
CategoryTheory.Limits.PreservesFiniteColimits
A functor is said to preserve finite colimits, if it preserves all colimits of
shape J, where J : Type is a finite category.
- Shape
- One type argument · adds preservesFiniteColimits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances14
- CategoryTheory.Functor
- ModuleCat
- HomologicalComplex
- Action
- Rep
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.ShortComplex
- FGModuleCat
- FintypeCat
- FDRep
- CategoryTheory.MorphismProperty.Under
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by112
- CategoryTheory.ShortComplex.ShortExact.map_of_exact
- CategoryTheory.Functor.mapDerivedCategory
- CategoryTheory.Abelian.Ext.mapExactFunctor
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor
- CategoryTheory.Functor.leftDerivedZeroIsoSelf
- CategoryTheory.Functor.mapDerivedCategoryFactors
- CategoryTheory.Functor.mapExtAddHom
- CategoryTheory.Abelian.Ext.mapExactFunctor_hom
- CategoryTheory.CostructuredArrow.projectQuotient
- CategoryTheory.Functor.mapExtLinearMap
- CategoryTheory.Limits.preservesFiniteColimits_of_natIso
- CategoryTheory.Abelian.Ext.mapExactFunctor.congr_simp
- CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀
- CategoryTheory.Abelian.Ext.mapExactFunctor_comp
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'
- CategoryTheory.Abelian.Ext.mapExactFunctor₀
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc
- CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms
- CategoryTheory.RightExactFunctor.of
- CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app
- CategoryTheory.Abelian.Ext.mapExactFunctor_extClass
- CategoryTheory.ExactFunctor.of
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app
- CategoryTheory.Functor.mapDerivedCategoryFactorsh
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc
- CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff
- CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff
- CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id
- CategoryTheory.DerivedCategory.map_triangleOfSESδ
- CategoryTheory.Limits.preservesFiniteLimits_op
- CategoryTheory.coflat_of_preservesFiniteColimits
- CategoryTheory.HasExactLimitsOfShape.domain_of_functor
- CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app
- CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app
- CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc
- CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id
- CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ
- CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality
- CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits
- CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves
- CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors
- CategoryTheory.Functor.mapExtAddHom.congr_simp
- CategoryTheory.Limits.preservesFiniteLimits_of_leftOp
- CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh
- CategoryTheory.Limits.preservesFiniteLimits_of_unop
- CategoryTheory.Limits.preservesFiniteLimits_unop
- CategoryTheory.CostructuredArrow.lift_projectQuotient
- CategoryTheory.Limits.preservesFiniteLimits_leftOp
- CategoryTheory.CostructuredArrow.projectQuotient_mk
Ancestors0
No ancestors.