grpObjObj

Mathlib.CategoryTheory.Monoidal.Grp_

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

Lean4

/-- The image of a group object under a monoidal functor is a group object. -/
abbrev grpObjObj {G : C} [GrpObj G] : GrpObj (F.obj G)
    where
  inv := F.map ι
  left_inv := by
    simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc, Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]
  right_inv := by
    simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc, Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]

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

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

Разделы

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

Аффилиация

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