functorToCore

Mathlib.CategoryTheory.Core

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Core.functorToCore

Lean4

/-- A functor from a groupoid to a category C factors through the core of C. -/
@[simps!]
def functorToCore (F : G ⥤ C) : G ⥤ Core C where
  obj X := .mk <| F.obj X
  map f := .mk <| { hom := F.map f, inv := F.map (Groupoid.inv f) }

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

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

Разделы

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

Аффилиация

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