evalOp

Mathlib.CategoryTheory.Limits.FormalCoproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.FormalCoproduct.evalOp

Lean4

/-- A presheaf valued in a category `A` with arbitrary products can be extended to the category of
formal coproducts. -/
@[simps!]
def evalOp : (Cᵒᵖ ⥤ A) ⥤ ((FormalCoproduct.{w} C)ᵒᵖ ⥤ A)
    where
  obj
    F :=
    { obj X := ∏ᶜ fun (i : X.unop.I) ↦ F.obj (op (X.unop.obj i))
      map f := Pi.lift fun i ↦ Pi.π _ (f.unop.f i) ≫ F.map (f.unop.φ i).op }
  map α := { app f := Pi.map fun i ↦ α.app (op (f.unop.obj i)) }

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

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

Разделы

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

Аффилиация

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