leftDerivedZeroIsoSelf — Mathlib

English

There is a canonical isomorphism F.leftDerived 0 ≅ F when F preserves finite colimits (right exactness).

Русский

Существует канонический изоморфизм F.leftDerived 0 ≅ F, если F сохраняет конечные колимиты (то есть правую точность).

LaTeX

$$$F.leftDerived 0 \\cong F$$$

Lean4

/-- The canonical isomorphism `F.leftDerived 0 ≅ F` when `F` is right exact
(i.e. preserves finite colimits). -/
@[simps! hom]
noncomputable def leftDerivedZeroIsoSelf : F.leftDerived 0 ≅ F :=
  (asIso F.fromLeftDerivedZero)

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