English
There is an equivalence: a functor F has a right derived functor along W if and only if a left Kan extension along L exists; formal statement: isRightDerivedFunctor_iff_isIso_rightDerivedDesc expresses that G.IsRightDerivedFunctor β W is equivalent to IsIso (RF.rightDerivedDesc α W G β).
Русский
Существует эквивалентность: существование правного производного функторa F вдоль W эквивалентно существованию левого Кан-расширения вдоль L; формальное утверждение isRightDerivedFunctor_iff_isIso_rightDerivedDesc выражает эквивалентность между G.IsRightDerivedFunctor β W и IsIso (RF.rightDerivedDesc α W G β).
LaTeX
$$G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)$$
Lean4
theorem hasRightDerivedFunctor_iff : F.HasRightDerivedFunctor W ↔ HasLeftKanExtension L F :=
by
have : HasRightDerivedFunctor F W ↔ HasLeftKanExtension W.Q F := ⟨fun h => h.hasLeftKanExtension', fun h => ⟨h⟩⟩
rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]
