comp_mk₀_id

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.Ext.comp_mk₀_id

English

Equivalently, composing with mk₀(id_Y) on the left yields α: (mk₀ id_Y).comp α (add_zero n) = α.

Русский

Аналогично с другой стороны: (mk₀ id_Y) . α = α.

LaTeX

$$$(mk_0(\\mathrm{id}_Y)).\\mathrm{comp} \\alpha (\\mathrm{add\\_zero}\\ n) = \\alpha$$$

Lean4

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

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

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

Разделы

Аффилиация

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