pointwiseRightKanExtension — Mathlib

Lean4
/-- The constructed pointwise right Kan extension
when `HasPointwiseRightKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseRightKanExtension : D ⥤ H
    where
  obj Y := limit (StructuredArrow.proj Y L ⋙ F)
  map {Y₁ Y₂}
    f :=
    limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
      (Cone.mk (limit (StructuredArrow.proj Y₁ L ⋙ F))
        { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g)
          naturality := fun g₁ g₂ φ ↦ by
            simpa using (limit.w (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).map φ)).symm })
  map_id
    Y :=
    limit.hom_ext
      (fun j => by
        dsimp
        simp only [limit.lift_π, id_comp]
        congr
        apply StructuredArrow.map_id)
  map_comp {Y₁ Y₂ Y₃} f
    f' :=
    limit.hom_ext
      (fun j => by
        dsimp
        simp only [limit.lift_π, assoc]
        congr 1
        apply StructuredArrow.map_comp)
Похожие утверждения