id_hom₂

Mathlib.CategoryTheory.Triangulated.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pretriangulated.id_hom₂

English

For the identity triangle, the hom₂ component is the identity on the second object.

Русский

Для тождественного треугольника компонент hom₂ равен тождественному морфизму на втором объекте.

LaTeX

$$$\mathrm{Triangle}.hom_{2}(\mathrm{Id}(A)) = \mathrm{Id}_{A_{2}}$$$

Lean4

@[simp]
theorem id_hom₂ (A : Triangle C) : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 _ :=
  rfl

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

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

Разделы

Аффилиация

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