diagonal_isomorphisms — Mathlib

English

In a category with pullbacks, the diagonal of the isomorphisms coincides with the diagonal of the monomorphisms.

Русский

В категории с перетягиванием (pullback) диагональ изоморфизмов совпадает с диагональю монохомоморфизмов.

LaTeX

$$$(\mathrm{isomorphisms}\, C).\mathrm{diagonal} = \mathrm{monomorphisms}\, C$$$

Lean4

theorem diagonal_isomorphisms : (isomorphisms C).diagonal = monomorphisms C :=
  ext _ _ fun _ _ _ ↦ pullback.isIso_diagonal_iff _

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