neg_hom

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.Ext.neg_hom

English

The negation on Ext corresponds to the negation on hom: (-α).hom = -α.hom.

Русский

Отрицание Ext соответствует отрицанию гом: (-α).hom = -α.hom.

LaTeX

$$$(-\\alpha).hom = -\\alpha.hom$$$

Lean4

theorem neg_hom (α : Ext X Y n) : (-α).hom = -α.hom := by
  rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]

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

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

Разделы

Аффилиация

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