coneAt

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

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

Lean4

/-- The cone for `StructuredArrow.proj Y L ⋙ F` attached to `E : RightExtension L F`.
The point of this cone is `E.left.obj Y` -/
@[simps]
def coneAt (Y : D) : Cone (StructuredArrow.proj Y L ⋙ F)
    where
  pt := E.left.obj Y
  π :=
    { app := fun g ↦ E.left.map g.hom ≫ E.hom.app g.right
      naturality := fun g₁ g₂ φ ↦ by
        dsimp
        rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]
        congr 1
        apply E.hom.naturality }

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

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

Разделы

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

Аффилиация

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