instIsIsoFunctorToRightDerivedZero

Mathlib.CategoryTheory.Abelian.RightDerived

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsIsoFunctorToRightDerivedZero

English

For a left-exact functor F, F.toRightDerivedZero is canonically isomorphic to F via the right-derived construction.

Русский

Для левосторонне точного функторa F отображение toRightDerivedZero явно изоморфно F через построение правой производной.

LaTeX

$$IsIso (F.toRightDerivedZero)$$

Lean4

instance : IsIso F.toRightDerivedZero :=
  NatIso.isIso_of_isIso_app _

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

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

Разделы

Аффилиация

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