isLeftAdjoint_of_preservesColimits

English

If L preserves colimits, then a corresponding left adjoint exists.

Русский

Если L сохраняет колимиты, то существует соответствующий левый смежник.

LaTeX

$$$\text{If } L \text{ preserves colimits, then } L \text{ is left adjoint}$$$

Lean4

/-- If `L` preserves colimits and `ℰ` has them, then it is a left adjoint. Note this is a (partial)
converse to `leftAdjointPreservesColimits`.
-/
theorem isLeftAdjoint_of_preservesColimits (L : (C ⥤ Type max w v₁ v₂) ⥤ ℰ)
    [PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂} L]
    [uliftYoneda.{max w v₂}.HasPointwiseLeftKanExtension
        (uliftYoneda.{max w v₂} ⋙ (opOpEquivalence C).congrLeft.functor.comp L)] :
    L.IsLeftAdjoint :=
  ⟨_,
    ⟨((opOpEquivalence C).congrLeft.symm.toAdjunction.comp (uliftYonedaAdjunction _ (𝟙 _))).ofNatIsoLeft
        ((opOpEquivalence C).congrLeft.invFunIdAssoc L)⟩⟩

Похожие утверждения