instIsIsoAppToRightDerivedZero — Mathlib

English

The canonical morphism F.toRightDerivedZero.app X is an isomorphism for all X when F preserves finite limits and colimits.

Русский

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

LaTeX

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

Lean4

instance (X : C) : IsIso (F.toRightDerivedZero.app X) :=
  by
  dsimp [Functor.toRightDerivedZero]
  infer_instance

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