mk₀_zero

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.Ext.mk₀_zero

English

The mk₀ map sends the zero morphism to the zero extension: mk₀(0) = 0 in Ext X Y n.

Русский

Мэп mk₀ отправляет нулевую стрелку в нулевое расширение: mk₀(0) = 0.

LaTeX

$$$mk_0(0: X\\to Y) = 0$$$

Lean4

@[simp]
theorem mk₀_zero : mk₀ (0 : X ⟶ Y) = 0 := by letI := HasDerivedCategory.standard C; ext; simp [zero_hom']

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

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

Разделы

Аффилиация

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