leftDerived — Mathlib

English

The left derived functors LF^n of an additive functor F are obtained by composing F with a projective resolution and then taking the nth homology.

Русский

Левые производные LF^n аддитивного функторa F получаются как композиция F с проективным разрешением и взятие n-й гомологии.

LaTeX

$$$\text{LF}_n(F) = H_n( F\circ P^\bullet) ,\quad P^\bullet \text{ projective resolution}.$$$

Lean4

/-- The left derived functors of an additive functor. -/
noncomputable def leftDerived (F : C ⥤ D) [F.Additive] (n : ℕ) : C ⥤ D :=
  F.leftDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D _ n

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