adj

Mathlib.Algebra.Category.Grp.Adjunctions

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

Lean4

/-- The free-forgetful adjunction for abelian groups.
-/
def adj : free ⊣ forget AddCommGrpCat.{u} :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => ConcreteCategory.homEquiv.trans FreeAbelianGroup.lift.symm
      homEquiv_naturality_left_symm := by
        intros
        ext
        simpa using FreeAbelianGroup.lift_comp .. }

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

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

Разделы

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

Аффилиация

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