mk₀_id_comp

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

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

English

Composition with the identity morphism on Y acts as identity on α: α . mk₀(id_Y) = α with appropriate degree shift.

Русский

Композиция с тождеством на Y действует как тождество: α . mk₀(id_Y) = α.

LaTeX

$$$\\alpha . mk_0(\\mathrm{id}_Y) = \\alpha$$$

Lean4

@[simp]
theorem mk₀_id_comp (α : Ext X Y n) : (mk₀ (𝟙 X)).comp α (zero_add n) = α := by letI := HasDerivedCategory.standard C;
  ext; simp

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

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

Разделы

Аффилиация

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