structuredArrowMapCone

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

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

Lean4

/-- An auxiliary cocone used in the lemma `pointwiseRightKanExtension_lift_app` -/
@[simps]
def structuredArrowMapCone (G : D ⥤ H) (α : L ⋙ G ⟶ F) (Y : D) : Cone (StructuredArrow.proj Y L ⋙ F)
    where
  pt := G.obj Y
  π :=
    { app := fun f ↦ G.map f.hom ≫ α.app f.right
      naturality := by simp [← α.naturality, ← G.map_comp_assoc] }

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

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

Разделы

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

Аффилиация

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