closedCounit

Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid

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

Lean4

/-- Auxiliary definition for `CategoryTheory.Functor.closed`.
The counit for the adjunction `(tensorLeft F) ⊣ (ihom F)`. -/
@[simps]
def closedCounit (F : D ⥤ C) : closedIhom F ⋙ tensorLeft F ⟶ 𝟭 (D ⥤ C) where
  app
    G :=
    { app := fun X => (ihom.ev (F.obj X)).app (G.obj X)
      naturality := by
        intro X Y f
        dsimp
        simp only [closedIhom_obj_map, pre_comm_ihom_map]
        rw [tensorHom_def]
        simp }

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

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

Разделы

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

Аффилиация

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