colimitCocone

Mathlib.Algebra.Category.Grp.Colimits

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

Lean4

/-- (internal implementation) The colimit cocone of a functor `F`, implemented as a quotient of
`DFinsupp (fun j ↦ F.obj j)`, under the assumption that said quotient is small.
-/
@[simps pt ι_app]
noncomputable def colimitCocone [DecidableEq J] [Small.{w} (Quot.{w} F)] : Cocone F
    where
  pt := AddCommGrpCat.of (Shrink (Quot F))
  ι :=
    { app j := AddCommGrpCat.ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F j))
      naturality _ _
        _ := by
        ext
        dsimp
        change Shrink.addEquiv.symm _ = _
        rw [Quot.map_ι] }

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

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

Разделы

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

Аффилиация

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