hasPointwiseRightDerivedFunctor_of_inverts

English

For L localized at W, a right-derived functor condition is equivalent to the left Kan extension condition along RF.

Русский

При локализации L относительно W условие правого производного функторa равно условию левого Кан-расширения вдоль RF.

LaTeX

$$[L.IsLocalization(W)] \Rightarrow [RF.IsRightDerivedFunctor(α,W) \iff RF.IsLeftKanExtension(α)]$$

Lean4

theorem hasPointwiseRightDerivedFunctor_of_inverts (F : C ⥤ H) {W : MorphismProperty C} (hF : W.IsInvertedBy F) :
    F.HasPointwiseRightDerivedFunctor W := by
  intro X
  rw [hasPointwiseRightDerivedFunctorAt_iff F W.Q W]
  exact
    (isPointwiseLeftKanExtensionOfIsoOfIsLocalization W (Localization.fac F hF W.Q).symm).hasPointwiseLeftKanExtension _

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