isPointwiseRightKanExtensionRanCounit

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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

Lean4

/-- If there exists a pointwise right Kan extension of `F` along `L`,
then `L.ran.obj G` is a pointwise right Kan extension of `F`. -/
noncomputable def isPointwiseRightKanExtensionRanCounit (F : C ⥤ H) [HasPointwiseRightKanExtension L F] :
    (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension :=
  isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (L.ranCounit.app F)

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

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

Разделы

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

Аффилиация

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