Mathlib Map

Structures · Category theory

CategoryTheory.Limits.ReflectsColimitsOfSize

A functor F : C ⥤ D reflects colimits if whenever the image of a cocone over some K : J ⥤ C 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.

Defined in
Mathlib.CategoryTheory.Limits.Preserves.Basic
Shape
One type argument · adds reflectsColimitsOfShape

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • Rep

How is a type an instance?

Loading the hierarchy index…

Assumed by19

Ancestors0

No ancestors.