Preservation of colimits on reflective targets #
This file applies the generic composition result to an ordinary adjunction of
functors whose counit is invertible. The theorem remains in Mathlib's
CategoryTheory.Adjunction namespace because it extends that structure, while
its physical owner is limit-preservation theory.
theorem
CategoryTheory.Adjunction.preservesColimitsOfShape_of_comp_left
{C : Type u_1}
[Category.{u_6, u_1} C]
{D : Type u_2}
[Category.{u_7, u_2} D]
{E : Type u_3}
[Category.{u_8, u_3} E]
{L : Functor C D}
{G : Functor D C}
(adj : L ⊣ G)
[IsIso adj.counit]
(F : Functor D E)
{K : Type u_4}
[Category.{u_5, u_4} K]
[Limits.HasColimitsOfShape K C]
[Limits.PreservesColimitsOfShape K L]
[Limits.PreservesColimitsOfShape K (L.comp F)]
:
Transport along a reflector. If the counit of L ⊣ G is invertible — so D is a
reflective target of L — then a functor F out of D preserves colimits of shape K as
soon as L and L ⋙ F do.
Every d : K ⥤ D is isomorphic to (d ⋙ G) ⋙ L, and
Limits.preservesColimit_comp_left applies to d ⋙ G.