isPointwiseLeftKanExtensionOfIsoOfIsLocalization

Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

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

Lean4

/-- If `L` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.hom` makes `G` a poinwise left Kan extension of `F` along `L`. -/
noncomputable def isPointwiseLeftKanExtensionOfIsoOfIsLocalization {G : D ⥤ H} (e : F ≅ L ⋙ G) [L.IsLocalization W] :
    (LeftExtension.mk _ e.hom).IsPointwiseLeftKanExtension := fun Y ↦
  have := Localization.essSurj L W
  (LeftExtension.mk _ e.hom).isPointwiseLeftKanExtensionAtEquivOfIso' (L.objObjPreimageIso Y)
    (isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization W e _)

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

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

Разделы

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

Аффилиация

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