ofCocone

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cotrident.ofCocone

Lean4

/-- Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
    `parallelFamily (F.map left) (F.map right)` and a cocone on `F`, we get a cotrident on
    `fun j ↦ F.map (line j)`. -/
def ofCocone {F : WalkingParallelFamily J ⥤ C} (t : Cocone F) : Cotrident fun j => F.map (line j)
    where
  pt := t.pt
  ι :=
    { app := fun X => eqToHom (by cases X <;> cat_disch) ≫ t.ι.app X
      naturality := by rintro _ _ (_ | _) <;> cat_disch }

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

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

Разделы

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

Аффилиация

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