cone

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsEventuallyConstantTo.cone

Lean4

/-- Given `h : F.IsEventuallyConstantTo i₀`, this is the (limit) cone for `F` whose
point is `F.obj i₀`. -/
@[simps]
noncomputable def cone : Cone F where
  pt := F.obj i₀
  π :=
    { app := h.coneπApp
      naturality := fun j j' φ ↦ by
        dsimp
        rw [id_comp]
        let i := IsCofiltered.min i₀ j
        let α : i ⟶ i₀ := IsCofiltered.minToLeft _ _
        let β : i ⟶ j := IsCofiltered.minToRight _ _
        rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp] }

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

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

Разделы

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

Аффилиация

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