hasPointwiseRightDerivedFunctorAt_iff

English

For a fixed X, F has a pointwise right derived functor at X iff F has a pointwise left Kan extension at L of X.

Русский

Для фиксированного X, F имеет точечное правое производное на X тогда и только тогда, когда F имеет точечное левое Кан-расширение на L в X.

LaTeX

$$$$ F.HasPointwiseRightDerivedFunctorAt W X \\iff HasPointwiseLeftKanExtensionAt L F (L.obj X). $$$$

Lean4

theorem hasPointwiseRightDerivedFunctorAt_iff [L.IsLocalization W] (X : C) :
    F.HasPointwiseRightDerivedFunctorAt W X ↔ HasPointwiseLeftKanExtensionAt L F (L.obj X) :=
  by
  rw [←
    hasPointwiseLeftKanExtensionAt_iff_of_equivalence W.Q L F (Localization.uniq W.Q L W)
      (Localization.compUniqFunctor W.Q L W) (W.Q.obj X) (L.obj X) ((Localization.compUniqFunctor W.Q L W).app X)]
  exact ⟨fun h ↦ h.hasColimit', fun h ↦ ⟨h⟩⟩

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