coprodObj

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.coprodObj

Lean4

/-- Auxiliary definition for `Over.coprod`. -/
@[simps]
noncomputable def coprodObj [HasBinaryCoproducts C] {A : C} : Over A → Over A ⥤ Over A := fun f =>
  { obj := fun g => Over.mk (coprod.desc f.hom g.hom)
    map := fun k => Over.homMk (coprod.map (𝟙 _) k.left) }

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

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

Разделы

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

Аффилиация

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