ofCone

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Trident.ofCone

Lean4

/-- Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
    `parallelFamily (fun j ↦ F.map (line j))` and a cone on `F`, we get a trident on
    `fun j ↦ F.map (line j)`. -/
def ofCone {F : WalkingParallelFamily J ⥤ C} (t : Cone F) : Trident fun j => F.map (line j)
    where
  pt := t.pt
  π :=
    { app := fun X => t.π.app X ≫ eqToHom (by cases X <;> cat_disch)
      naturality := by rintro _ _ (_ | _) <;> cat_disch }

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

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

Разделы

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

Аффилиация

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