rightDerivedZeroIsoSelf — Mathlib

English

There exists a canonical isomorphism between F.rightDerived 0 and F when F preserves finite limits.

Русский

Существует канонический изоморфизм между F.rightDerived 0 и F при сохранении конечных пределов.

LaTeX

$$F.rightDerivedZeroIsoSelf : F.rightDerived 0 ≅ F$$

Lean4

/-- The canonical isomorphism `F.rightDerived 0 ≅ F` when `F` is left exact
(i.e. preserves finite limits). -/
@[simps! inv]
noncomputable def rightDerivedZeroIsoSelf : F.rightDerived 0 ≅ F :=
  (asIso F.toRightDerivedZero).symm

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