isRightDerivedFunctor_iff_isLeftKanExtension

English

Given a family RF, RF', RF'' of functors D ⥤ H and a natural isomorphism e: F ≅ F', the right-derived functor along RF is equivalent to a left Kan extension along α when L is localized and the coherence condition holds.

Русский

При наличии функторов RF, RF'' и изоморфизма e: F ≅ F', производная справа вдоль RF эквивалентна левому кан-расширению вдоль α при локализации L и согласованности.

LaTeX

$$\forall {L IsLocalization W} [RF.IsRightDerivedFunctor α W] , RF.IsRightDerivedFunctor α W \iff RF.IsLeftKanExtension α$$

Lean4

theorem isRightDerivedFunctor_iff_isLeftKanExtension [L.IsLocalization W] :
    RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α :=
  by
  constructor
  · exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W
  · exact fun h => ⟨h⟩

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