Relations

Mathlib.Algebra.Category.Grp.Colimits

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.Colimits.Relations

Lean4

/-- The relations between elements of the direct sum of the `F.obj j` given by the
morphisms in the diagram `J`.
-/
abbrev Relations [DecidableEq J] : AddSubgroup (DFinsupp (fun j ↦ F.obj j)) :=
  AddSubgroup.closure
    {x | ∃ (j j' : J) (u : j ⟶ j') (a : F.obj j), x = DFinsupp.single j' (F.map u a) - DFinsupp.single j a}

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

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

Разделы

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

Аффилиация

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