otherMap

Mathlib.CategoryTheory.Adjunction.Lifting.Right

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LiftRightAdjoint.otherMap

Lean4

/-- (Implementation)
To construct the right adjoint, we use the equalizer of `U' F η_X` with the composite

`U' F X ⟶ U' F L U' F X ⟶ U' F U F L U' F X ⟶ U' F U F X`

where the first morphism is `ι_U'FX`, the second is `U' F η_LU'FX` and the third is `U' F U δ_FX`.
We will show that this equalizer exists and that it forms the object map for a right adjoint to `L`.
-/
def otherMap (X : B) : U'.obj (F.obj X) ⟶ U'.obj (F.obj (U.obj (F.obj X))) :=
  adj₂.unit.app _ ≫ U'.map (F.map (adj₁.unit.app _ ≫ (U.map (adj₂.counit.app _))))

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

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

Разделы

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

Аффилиация

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