partialLeftAdjointMap

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

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

Lean4

/-- Given `F : D ⥤ C`, this is `F.partialLeftAdjoint` on morphisms. -/
noncomputable def partialLeftAdjointMap {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y) :
    F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Y :=
  F.partialLeftAdjointHomEquiv.symm (f ≫ F.partialLeftAdjointHomEquiv (𝟙 _))

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

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

Разделы

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

Аффилиация

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