rightDerivedToHomotopyCategory_id

English

The right-derived functor applied to the identity natural transformation is the identity on the right-derived functor.

Русский

Правые производные функторa, применённые к тождественному преобразованию, дают тождество на правой производной.

LaTeX

$$$\\mathrm{rightDerived}(\\mathrm{id}_F) = \\mathrm{id}_{F^{\\mathrm{rightDerived}}}$$$

Lean4

@[simp]
theorem rightDerivedToHomotopyCategory_id (F : C ⥤ D) [F.Additive] :
    NatTrans.rightDerivedToHomotopyCategory (𝟙 F) = 𝟙 _ :=
  rfl

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