closedUnit

Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid

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

Lean4

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

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

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

Разделы

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

Аффилиация

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