rightDerivedZeroIsoSelf_inv_hom_id_app

English

For any F that preserves finite limits, the natural isomorphism F.toRightDerivedZero' app X is an isomorphism for each X.

Русский

Для любого F, сохраняющего конечные пределы, отображение F.toRightDerivedZero' app X является изоморфизмом для каждого X.

LaTeX

$$IsIso (F.toRightDerivedZero' F).app X$$

Lean4

@[reassoc (attr := simp)]
theorem rightDerivedZeroIsoSelf_inv_hom_id_app (X : C) :
    F.toRightDerivedZero.app X ≫ F.rightDerivedZeroIsoSelf.hom.app X = 𝟙 _ :=
  F.rightDerivedZeroIsoSelf.inv_hom_id_app X

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