id_map

Mathlib.CategoryTheory.Shift.ShiftedHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShiftedHom.id_map

English

Let f be a ShiftedHom X Y a. The action of the identity functor preserves f; that is, f.map Id_C = f.

Русский

Пусть f — ShiftedHom X Y a. Действие тождественного функторa сохраняет f; то есть f.map Id_C = f.

LaTeX

$$$f.map(\\mathrm{Id}_C) = f$$$

Lean4

@[simp]
theorem id_map {a : M} (f : ShiftedHom X Y a) : f.map (𝟭 C) = f := by
  simp [map, Functor.commShiftIso, Functor.CommShift.iso]

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

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

Разделы

Аффилиация

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