Structures · Category theory
CategoryTheory.Limits.ReflectsColimit
A functor F : C ⥤ D reflects colimits for K : J ⥤ C if
whenever the image of a cocone over K under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
- Shape
- 2 explicit arguments · adds reflects
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- ModuleCat
- Action
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- CategoryTheory.Limits.isColimitOfReflects
- CategoryTheory.Limits.IsInitial.isInitialIffObj
- CategoryTheory.IsPushout.of_map
- CategoryTheory.Limits.ReflectsColimit.reflects
- CategoryTheory.Limits.IsInitial.isInitialOfObj
- CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves
- CategoryTheory.Limits.reflectsLimit_of_leftOp
- CategoryTheory.Limits.reflectsLimit_of_op
- CategoryTheory.Functor.Final.reflectsColimit_of_comp
- CategoryTheory.Limits.reflectsLimit_unop
- CategoryTheory.Limits.reflectsLimit_of_unop
- CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap
- CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects
- CategoryTheory.Square.IsPushout.of_map
- CategoryTheory.Limits.reflectsLimit_op
- CategoryTheory.Limits.reflectsLimit_leftOp
- CategoryTheory.Limits.reflectsLimit_rightOp
- CategoryTheory.Limits.reflectsLimit_of_rightOp
- CategoryTheory.Limits.reflectsColimit_of_natIso
- CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer
- CategoryTheory.Functor.Final.comp_reflectsColimit
- CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj
- CategoryTheory.IsPushout.of_map_of_faithful
- CategoryTheory.reflects_epi_of_reflectsColimit
- CategoryTheory.IsPushout.map_iff
- CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit
- CategoryTheory.Limits.IsInitial.isInitialOfObj.congr_simp
- CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects
- CategoryTheory.Square.IsPushout.map_iff
- CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial
- CategoryTheory.Limits.comp_reflectsColimit
- CategoryTheory.Limits.isColimitOfIsColimitCoforkMap
- CategoryTheory.Limits.reflectsColimit_of_iso_diagram
Ancestors0
No ancestors.