attachCellsιFunctorObj

Mathlib.CategoryTheory.SmallObject.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.attachCellsιFunctorObj

Lean4

/-- The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is obtained by
attaching `f`-cells. -/
@[simps]
noncomputable def attachCellsιFunctorObj : AttachCells.{max v w} f (ιFunctorObj f πX)
    where
  ι := FunctorObjIndex f πX
  π x := x.i
  isColimit₁ := coproductIsCoproduct _
  isColimit₂ := coproductIsCoproduct _
  m := functorObjLeft f πX
  g₁ := functorObjTop f πX
  g₂ := ρFunctorObj f πX
  isPushout := IsPushout.of_hasPushout (functorObjTop f πX) (functorObjLeft f πX)
  cofan₁ := _
  cofan₂ := _

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

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

Разделы

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

Аффилиация

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