colimitCoconeIsColimit

Mathlib.Algebra.Category.Grp.Colimits

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

Lean4

/-- (internal implementation) The fact that the candidate colimit cocone constructed in
`colimitCocone` is the colimit.
-/
noncomputable def colimitCoconeIsColimit [DecidableEq J] [Small.{w} (Quot F)] : IsColimit (colimitCocone F) :=
  by
  refine isColimit_of_bijective_desc F _ ?_
  rw [Quot.desc_colimitCocone]
  exact Shrink.addEquiv.symm.bijective

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

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

Разделы

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

Аффилиация

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