isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization

Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

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

← MathLib Explorer

Lean4

/-- Let `L : C ⥤ D` be a localization functor for `W`, if an extension `E`
of `F : C ⥤ H` along `L` is such that the natural transformation
`E.hom : F ⟶ L ⋙ E.right` is an isomorphism, then `E` is a pointwise
left Kan extension. -/
noncomputable def isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization (E : LeftExtension L F) [IsIso E.hom]
    [L.IsLocalization W] : E.IsPointwiseLeftKanExtension :=
  Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization W (asIso E.hom)

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

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

Разделы

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

Аффилиация

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