id_hom

Mathlib.CategoryTheory.Action.Basic

URI: https://scilib.ai/kg/mathlib#Action.id_hom

English

The map underlying the identity action morphism is the identity on objects.

Русский

Базовая карта тождественного действия равна тождественному отображению на объекте.

LaTeX

$$$ (\mathsf{1}_M : Hom M M).hom = \mathrm{id}_{M.V}$$$

Lean4

@[simp]
theorem id_hom (M : Action V G) : (𝟙 M : Hom M M).hom = 𝟙 M.V :=
  rfl

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

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

Разделы

Аффилиация

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