map_η_ε

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.map_η_ε

English

Composite of maps ε and η under a monoidal functor is identity after mapping.

Русский

Сложение ε и η под моноидального функторa дает тождество после отображения.

LaTeX

$$$G.map(\\varepsilon F) \\circ G.map(\\eta F) = \\mathrm{Id}$$$

Lean4

@[reassoc (attr := simp)]
theorem map_η_ε (G : D ⥤ C') : G.map (η F) ≫ G.map (ε F) = 𝟙 _ :=
  (εIso F).map_inv_hom_id G

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

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

Разделы

Аффилиация

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