isLeftDerivedFunctor_iff_of_iso — Mathlib

English

Left-derived-functor property is preserved under isomorphism of the target functor, i.e., if LF ≅ LF', then LF is left-derived w.r.t. α and W if and only if LF' is.

Русский

Свойство левый производной_functor сохраняется при изоморфизме целевого функторa: если LF ≅ LF', то LF будет слева-образовательной относительно α и W тогда и только тогда LF'.

LaTeX

$$$$ \\text{LF.IsLeftDerivedFunctor } \\alpha \\, W \\iff \\text{LF'.IsLeftDerivedFunctor } \\alpha' \\, W $$$$

Lean4

theorem isLeftDerivedFunctor_iff_of_iso (α' : L ⋙ LF' ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] (e : LF ≅ LF')
    (comm : whiskerLeft L e.hom ≫ α' = α) : LF.IsLeftDerivedFunctor α W ↔ LF'.IsLeftDerivedFunctor α' W :=
  by
  simp only [isLeftDerivedFunctor_iff_isRightKanExtension]
  exact isRightKanExtension_iff_of_iso e _ _ comm

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