leftDerivedToHomotopyCategory_id

Mathlib.CategoryTheory.Abelian.LeftDerived

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id

English

The leftDerived functor at level 0 coincides with the original functor: leftDerived 0 ≅ F.

Русский

Левый производный при уровне 0 совпадает с исходным функтором: leftDerived 0 ≅ F.

LaTeX

$$$ (F.leftDerived 0) = F$ (up to canonical isomorphism)$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru