id_hcomp

Mathlib.CategoryTheory.Whiskering

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.id_hcomp

English

For F: C ⥤ D and α: G ⟶ H, 𝟙 F ◫ α equals whiskerLeft F α.

Русский

Для F: C ⥤ D и α: G ⟶ H, 𝟙 F ◫ α равно whiskerLeft F α.

LaTeX

$$$ 𝟙 F \\;\\square\\; α = \\mathrm{whiskerLeft} F α $$$

Lean4

@[simp]
theorem id_hcomp (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : 𝟙 F ◫ α = whiskerLeft F α :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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