piConstAdj

Mathlib.CategoryTheory.Limits.Shapes.Products

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.piConstAdj

Lean4

/-- `n ↦ ∏ₙ X` is left adjoint to `Hom(-, X)`. -/
def piConstAdj [Limits.HasProducts.{v} C] (X : C) : (piConst.obj X).rightOp ⊣ yoneda.obj X
    where
  unit := { app n i := Limits.Pi.π (fun _ : n ↦ X) i }
  counit := { app Y := (Limits.Pi.lift id).op, naturality _ _ _ := by apply Quiver.Hom.unop_inj; cat_disch }
  left_triangle_components _ := by apply Quiver.Hom.unop_inj; cat_disch

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

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

Разделы

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

Аффилиация

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