ι

Mathlib.Algebra.Category.Grp.Colimits

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

Lean4

/-- Inclusion of `F.obj j` into the candidate colimit.
-/
def ι [DecidableEq J] (j : J) : F.obj j →+ Quot F :=
  (QuotientAddGroup.mk' _).comp (DFinsupp.singleAddHom (fun j ↦ F.obj j) j)

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

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

Разделы

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

Аффилиация

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