mono_Δ

Mathlib.CategoryTheory.Abelian.NonPreadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonPreadditiveAbelian.mono_Δ

English

The diagonal Δ is a monomorphism: diag A is mono.

Русский

Диагональ Δ является мономорфизмом: diag A — моно.

LaTeX

$$$\\operatorname{Mono}(\\mathrm{diag}(A))$$$

Lean4

instance mono_Δ {A : C} : Mono (diag A) :=
  mono_of_mono_fac <| prod.lift_fst _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru