constructRightAdjointObj

Mathlib.CategoryTheory.Adjunction.Lifting.Right

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

Lean4

/-- Construct the object part of the desired right adjoint as the equalizer of `U'Fη_Y` with
`otherMap`.
-/
noncomputable def constructRightAdjointObj (Y : B) : C :=
  equalizer (U'.map (F.map (adj₁.unit.app Y))) (otherMap _ _ adj₁ adj₂ Y)

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

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

Разделы

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

Аффилиация

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