εIso

Mathlib.Algebra.Category.ModuleCat.Adjunctions

URI: https://scilib.ai/kg/mathlib#ModuleCat.FreeMonoidal.εIso

Lean4

/-- The canonical isomorphism `𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u))`.
(This should not be used directly: it is part of the implementation of the
monoidal structure on the functor `free R`.) -/
def εIso : 𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u))
    where
  hom := ofHom <| Finsupp.lsingle PUnit.unit
  inv := ofHom <| Finsupp.lapply PUnit.unit
  hom_inv_id := by
    ext
    simp [free]
  inv_hom_id := by
    ext ⟨⟩
    dsimp [freeMk]
    erw [Finsupp.lapply_apply, Finsupp.lsingle_apply]
    rw [Finsupp.single_eq_same]

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

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

Разделы

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

Аффилиация

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