isRightDerivedFunctor_iff_of_iso — Mathlib

English

If α: F → L ⋙ RF' and localization, then an isomorphism e: RF ≅ RF' yields that right-derived functors coincide with the left Kan extensions under a coherence condition.

Русский

Если есть изоморфизм e: RF ≅ RF' и локализация, то правые производные совпадают с левыми Кан-расширениями при согласованности.

LaTeX

$$[α, W][L.IsLocalization(W)] (e: RF ≅ RF') (comm : α ≫ whiskerLeft L e.hom = α') : RF.IsRightDerivedFunctor α W \iff RF'.IsRightDerivedFunctor α' W$$

Lean4

theorem isRightDerivedFunctor_iff_of_iso (α' : F ⟶ L ⋙ RF') (W : MorphismProperty C) [L.IsLocalization W] (e : RF ≅ RF')
    (comm : α ≫ whiskerLeft L e.hom = α') : RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W :=
  by
  simp only [isRightDerivedFunctor_iff_isLeftKanExtension]
  exact isLeftKanExtension_iff_of_iso e _ _ comm

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