ofFunctor

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.BasedCategory.ofFunctor

Lean4

/-- The based category associated to a functor `p : 𝒳 ⥤ 𝒮`. -/
def ofFunctor {𝒳 : Type u₂} [Category.{v₂} 𝒳] (p : 𝒳 ⥤ 𝒮) : BasedCategory 𝒮
    where
  obj := 𝒳
  p := p

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

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

Разделы

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

Аффилиация

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