Preservation of colimits and reflective adjunctions #
Let adj : F ⊣ G be an adjunction with G : D ⥤ C full and faithful.
We show that if colimits of shape J exist in C, then a functor
H : D ⥤ E preserves colimits of shape J iff F ⋙ H does.
In particular, a functor from a category of sheaves preserves colimits iff it does so after precomposition with the sheafification functor.
theorem
CategoryTheory.Adjunction.preservesColimitsOfShape_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
{E : Type u₃}
[Category.{v₃, u₃} E]
(H : Functor D E)
(J : Type u)
[Category.{v, u} J]
[Limits.HasColimitsOfShape J C]
[G.Full]
[G.Faithful]
:
theorem
CategoryTheory.Adjunction.preservesColimitsOfSize_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
{E : Type u₃}
[Category.{v₃, u₃} E]
(H : Functor D E)
[Limits.HasColimitsOfSize.{v, u, v₁, u₁} C]
[G.Full]
[G.Faithful]
: