prod'_η_fst

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.prod'_η_fst

English

The second component of η for the prod' construction equals η on G, under suitable context.

Русский

Вторая компонента η для prod' равна η для G в подходящем контексте.

LaTeX

$$$ (\eta_{\mathrm{prod}'}(F,G))_{2} = \eta_G $$$

Lean4

@[simp]
theorem prod'_η_fst : (η (prod' F G)).1 = η F :=
  by
  change F.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

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

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

Разделы

Аффилиация

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