isLimitEvalMapConeCofanOp

Mathlib.CategoryTheory.Limits.FormalCoproducts

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

Lean4

/-- `evalOp(F)` preserves arbitrary products. -/
def isLimitEvalMapConeCofanOp : IsLimit (((evalOp.{w} C A).obj F).mapCone (cofan.{w} J f).op)
    where
  lift s := Pi.lift fun i ↦ s.π.app ⟨i.1⟩ ≫ Pi.π _ i.2
  fac s i := Pi.hom_ext _ _ fun i ↦ by simp [cofan]
  uniq s m h := Pi.hom_ext _ _ fun ⟨i₁, i₂⟩ ↦ by simp [← h, cofan]

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

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

Разделы

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

Аффилиация

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