leftDerived — Mathlib

English

There is a canonical isomorphism between the left-derived object at X and the homology of the mapped complex, for any X and projective resolution P.

Русский

Существует канонический изоморфизм между левым производным объектом в X и гомологией образованного комплекса при любом X и проективном разрешении P.

LaTeX

$$$ (F.leftDerived n).obj X \cong H_n( (F.mapHomologicalComplex _).obj P.complex )$$$

Lean4

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

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