From 87c814e32360ebb12c3cf228b8cf0f52acd0ed24 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 10 Oct 2024 16:50:24 +0200 Subject: [PATCH] doc --- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean index e98b1cef802e1..a1a044d1a3846 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean @@ -103,6 +103,8 @@ namespace IsPointwiseLeftKanExtensionAt variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [HasColimit (CostructuredArrow.proj L Y ⋙ F)] +/-- A pointwise left Kan extension of `F` along `L` applied to an object `Y` is isomorphic to +`colimit (CostructuredArrow.proj L Y ⋙ F)`. -/ noncomputable def isoColimit : E.right.obj Y ≅ colimit (CostructuredArrow.proj L Y ⋙ F) := h.coconePointUniqueUpToIso (colimit.isColimit _) @@ -238,6 +240,8 @@ namespace IsPointwiseRightKanExtensionAt variable {E} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [HasLimit (StructuredArrow.proj Y L ⋙ F)] +/-- A pointwise right Kan extension of `F` along `L` applied to an object `Y` is isomorphic to +`limit (StructuredArrow.proj Y L ⋙ F)`. -/ noncomputable def isoLimit : E.left.obj Y ≅ limit (StructuredArrow.proj Y L ⋙ F) := h.conePointUniqueUpToIso (limit.isLimit _)