prod'_μ_snd

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.prod'_μ_snd

← MathLib Explorer

English

For objects X,Y in C, the first component of μ for prod' equals μ_F at X,Y.

Русский

Для объектов X,Y в C первая компонента μ для prod' равна μ_F(X,Y).

LaTeX

$$$ (\mu_{\mathrm{prod}'}(F,G))_{X,Y}^{1} = \mu_F(X,Y) $$$

Lean4

@[simp]
theorem prod'_μ_snd (X Y : C) : (μ (prod' F G) X Y).2 = μ G X Y :=
  by
  change _ ≫ G.map (𝟙 _) = _
  rw [Functor.map_id, Category.comp_id]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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