equiv

Mathlib.CategoryTheory.Limits.Cones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cone.equiv

Lean4

/-- The isomorphism between a cone on `F` and an element of the functor `F.cones`. -/
@[simps!]
def equiv (F : J ⥤ C) : Cone F ≅ Σ X, F.cones.obj X
    where
  hom c := ⟨op c.pt, c.π⟩
  inv
    c :=
    { pt := c.1.unop
      π := c.2 }
  hom_inv_id := by
    funext X
    cases X
    rfl
  inv_hom_id := by
    funext X
    cases X
    rfl

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

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

Разделы

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

Аффилиация

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