isoWhiskerRight_refl

Mathlib.CategoryTheory.Whiskering

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

English

Whiskering by a right identity is the identity morphism.

Русский

Свивка вправо по тождественному функтору — это тождественный морфизм.

LaTeX

$$$\\mathrm{isoWhiskerRight}(\\mathrm{Iso.refl}\,F)\,G = \\mathrm{Iso.refl}\, (F \\circ G)$$$

Lean4

@[simp]
theorem isoWhiskerRight_refl (F : C ⥤ D) (G : D ⥤ E) : isoWhiskerRight (Iso.refl F) G = Iso.refl _ := by cat_disch

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

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

Разделы

Аффилиация

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