derived — Mathlib

Lean4
/-- An adjunction between functors induces an adjunction between the
corresponding left/right derived functors, when these derived
functors are *absolute*, i.e. they remain derived functors
after the post-composition with any functor.

(One actually only needs that `G' ⋙ F'` is the left derived functor of
`G ⋙ L₂ ⋙ F'` and that `F' ⋙ G'` is the right derived functor of
`F ⋙ L₁ ⋙ G'`). -/
@[simps!]
noncomputable def derived [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂]
    [(G' ⋙ F').IsLeftDerivedFunctor ((Functor.associator _ _ _).inv ≫ whiskerRight α F') W₁]
    [(F' ⋙ G').IsRightDerivedFunctor (whiskerRight β G' ≫ (Functor.associator _ _ _).hom) W₂] : G' ⊣ F' :=
  adj.derived' W₁ W₂ α β (adj.derivedη W₁ α β) (adj.derivedε W₂ α β)
Похожие утверждения