Structures · Category theory
CategoryTheory.Limits.PreservesColimit
A functor F preserves colimits of K (written as PreservesColimit K F)
if F maps any colimit cocone over K to a colimit cocone.
- Shape
- 2 explicit arguments · adds preserves
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances11
- CategoryTheory.Functor
- ModuleCat
- HomologicalComplex
- Action
- AlgebraicGeometry.Scheme
- PresheafOfModules
- CategoryTheory.ShortComplex
- PartOrdEmb
- CategoryTheory.Limits.FormalCoproduct
- CategoryTheory.MorphismProperty.Over
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by321
- CategoryTheory.Limits.isColimitOfPreserves
- CategoryTheory.Limits.PreservesCoequalizer.iso
- CategoryTheory.preservesColimitIso
- CategoryTheory.Limits.PreservesCokernel.iso
- CategoryTheory.Limits.preservesColimit_of_iso_diagram
- CategoryTheory.Abelian.PreservesImage.iso
- CategoryTheory.Abelian.PreservesCoimage.iso
- CategoryTheory.Limits.PreservesPushout.iso
- CategoryTheory.GradedObject.mapBifunctorRightUnitor
- CategoryTheory.GradedObject.mapBifunctorLeftUnitor
- CategoryTheory.PreservesImage.iso
- CategoryTheory.GlueData.gluedIso
- CategoryTheory.GlueData.ι_gluedIso_inv
- CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator
- CategoryTheory.ι_preservesColimitIso_inv
- CategoryTheory.Limits.CokernelCofork.mapIsColimit
- CategoryTheory.Limits.preservesColimit_of_natIso
- CategoryTheory.Limits.PreservesCokernel.iso_inv
- CategoryTheory.GlueData.ι_jointly_surjective
- CategoryTheory.Functor.map_isPushout
- CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit
- CategoryTheory.Comma.coconeOfPreserves
- CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit
- CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso
- CategoryTheory.Limits.Concrete.isColimit_exists_rep
- CategoryTheory.IsPushout.map
- CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso
- CategoryTheory.Limits.PreservesCoproduct.iso
- CategoryTheory.GradedObject.Monoidal.leftUnitor
- PresheafOfModules.colimitPresheafOfModules
- CategoryTheory.Abelian.PreservesCoimageImageComparison.iso
- CategoryTheory.Limits.PreservesColimitPair.iso
- CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan
- CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_hom_left
- CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap
- CategoryTheory.GradedObject.Monoidal.rightUnitor
- CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan
- CategoryTheory.GlueData.hasColimit_mapGlueData_diagram
- CategoryTheory.Limits.IsInitial.isInitialObj
- CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit
- CategoryTheory.Monad.ForgetCreatesColimits.coconePoint
- CategoryTheory.ι_preservesColimitIso_hom
- CategoryTheory.Limits.isColimitCoforkMapOfIsColimit
- CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit
- CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit
- CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone
- CategoryTheory.Limits.Concrete.colimit_exists_rep
- CategoryTheory.Limits.IsInitial.isInitialIffObj
- HomologicalComplex.leftUnitor'
- CategoryTheory.Limits.map_π_preserves_coequalizer_inv
Ancestors0
No ancestors.