pointwiseRightKanExtensionCounit — Mathlib

Lean4

/-- The counit of the constructed pointwise right Kan extension when
`HasPointwiseRightKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseRightKanExtensionCounit : L ⋙ pointwiseRightKanExtension L F ⟶ F
    where
  app X := limit.π (StructuredArrow.proj (L.obj X) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X)))
  naturality {X₁ X₂}
    f :=
    by
    simp only [comp_obj, pointwiseRightKanExtension_obj, comp_map, pointwiseRightKanExtension_map, limit.lift_π,
      StructuredArrow.map_mk]
    rw [comp_id]
    let φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) := StructuredArrow.homMk f
    exact (limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

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