free

Mathlib.Algebra.Category.Grp.Adjunctions

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.free

Lean4

/-- The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
free abelian group with generators `x : X`.
-/
def free : Type u ⥤ AddCommGrpCat where
  obj α := of (FreeAbelianGroup α)
  map f := ofHom (FreeAbelianGroup.map f)
  map_id _ := AddCommGrpCat.ext FreeAbelianGroup.map_id_apply
  map_comp _ _ := AddCommGrpCat.ext FreeAbelianGroup.map_comp_apply

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

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

Разделы

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

Аффилиация

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