adj

Mathlib.Algebra.Category.MonCat.Adjunctions

URI: https://scilib.ai/kg/mathlib#AddCommMonCat.adj

Lean4

/-- The free-forgetful adjunction for commutative monoids. -/
noncomputable def adj : free ⊣ forget AddCommMonCat.{u}
    where
  unit := { app X i := Finsupp.single i 1 }
  counit :=
    { app M := ofHom (Finsupp.liftAddHom (multiplesHom M))
      naturality {M N} f := by dsimp; ext1; apply Finsupp.liftAddHom.symm.injective; ext; simp }

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

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

Разделы

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

Аффилиация

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