opcyclesMap_id

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.opcyclesMap_id

English

For the identity morphism on S, opcyclesMap yields the identity on the target.

Русский

Для тождественного отображения на S карта opcyclesMap даёт тождественный морфизм на целевом объекте.

LaTeX

$$opcyclesMap (id_S) = id$$

Lean4

@[simp]
theorem opcyclesMap_id [HasRightHomology S] : opcyclesMap (𝟙 S) = 𝟙 _ :=
  opcyclesMap'_id _

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

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

Разделы

Аффилиация

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