coyonedaAdj

Mathlib.Algebra.Category.Ring.Adjunctions

URI: https://scilib.ai/kg/mathlib#CommRingCat.coyonedaAdj

Lean4

/-- The adjunction `Hom_{CRing}(Fun(n, R), S) ≃ Fun(n, Hom_{CRing}(R, S))`. -/
def coyonedaAdj (R : CommRingCat.{u}) : (coyoneda.flip.obj R).rightOp ⊣ yoneda.obj R
    where
  unit := { app n i := CommRingCat.ofHom (Pi.evalRingHom _ i) }
  counit := { app S := (CommRingCat.ofHom (Pi.ringHom fun f ↦ f.hom)).op }

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

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

Разделы

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

Аффилиация

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