hasColimit — Mathlib

English

If F has a pointwise right derived functor at X, then F has a colimit structure providing the left Kan extension at L for X.

Русский

Если F имеет точечное правое производное в X, то F имеет структуру колимита, обеспечивающую левое Кан-расширение для X.

LaTeX

$$$$ [L.IsLocalization W] (X) [F.HasPointwiseRightDerivedFunctorAt W X] : HasPointwiseLeftKanExtensionAt L F (L.obj X). $$$$

Lean4

theorem hasColimit [L.IsLocalization W] (X : C) [F.HasPointwiseRightDerivedFunctorAt W X] :
    HasPointwiseLeftKanExtensionAt L F (L.obj X) := by rwa [← hasPointwiseRightDerivedFunctorAt_iff F L W]

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