isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor

Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

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

Lean4

/-- A right derived functor is a pointwise right derived functor when
there exists a pointwise right derived functor. -/
noncomputable def isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor [L.IsLocalization W]
    [F'.IsRightDerivedFunctor α W] : (LeftExtension.mk _ α).IsPointwiseLeftKanExtension :=
  have := hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor F L
  have := IsRightDerivedFunctor.isLeftKanExtension F' α W
  isPointwiseLeftKanExtensionOfIsLeftKanExtension F' α

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

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

Разделы

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

Аффилиация

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