rightUnitor_hom_app

Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

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

English

The hom component of the right unitor at F matches that at F(j) for each j.

Русский

Гомоморфия правого унитора в F совпадает с соответствующей компонентой для F(j) на каждом j.

LaTeX

$$$$ (\rho_ F).hom.app j = (\rho_{F(j)}).hom. $$$$

Lean4

@[simp]
theorem rightUnitor_hom_app (F : J ⥤ C) (j : J) : (ρ_ F).hom.app j = (ρ_ (F.obj j)).hom :=
  (rightUnitor_hom _).symm

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

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

Разделы

Аффилиация

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