rightDerived — Mathlib

English

Naturality of the inverse part of the right-derived object isomorphism with respect to f.

Русский

Естественность обратной части изоморфизма между правыми производными по f.

LaTeX

$$$(I.isoRightDerivedObj F n).inv \\circ F.rightDerived n .map f = \\cdots$$$

Lean4

/-- The natural transformation between right-derived functors
induced by a natural transformation. -/
noncomputable def rightDerived {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) :
    F.rightDerived n ⟶ G.rightDerived n :=
  Functor.whiskerRight (NatTrans.rightDerivedToHomotopyCategory α) _

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