yonedaGrpObj

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

URI: https://scilib.ai/kg/mathlib#yonedaGrpObj

Lean4

/-- If `G` is a group object, then `Hom(-, G)` is a presheaf of groups. -/
@[simps]
def yonedaGrpObj : Cᵒᵖ ⥤ GrpCat.{v} where
  obj X := GrpCat.of (unop X ⟶ G)
  map φ := GrpCat.ofHom ((yonedaMonObj G).map φ).hom

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

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

Разделы

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

Аффилиация

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