pointwiseRightKanExtensionIsPointwiseRightKanExtension

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

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

Lean4

/-- The functor `pointwiseRightKanExtension L F` is a pointwise right Kan
extension of `F` along `L`. -/
noncomputable def pointwiseRightKanExtensionIsPointwiseRightKanExtension :
    (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsPointwiseRightKanExtension := fun X =>
  IsLimit.ofIsoLimit (limit.isLimit _)
    (Cones.ext (Iso.refl _)
      (fun j => by
        dsimp
        simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]
        congr
        rw [comp_id, ← StructuredArrow.eq_mk]))

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

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

Разделы

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

Аффилиация

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