coneAtFunctor

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.RightExtension.coneAtFunctor

Lean4

/-- The cones for `StructuredArrow.proj Y L ⋙ F`, as a functor from `RightExtension L F`. -/
@[simps]
def coneAtFunctor (Y : D) : RightExtension L F ⥤ Cone (StructuredArrow.proj Y L ⋙ F)
    where
  obj E := E.coneAt Y
  map {E E'}
    φ :=
    ConeMorphism.mk (φ.left.app Y)
      (fun G ↦ by
        dsimp
        rw [← CostructuredArrow.w φ]
        simp)

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

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

Разделы

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

Аффилиация

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