isColimitConstCocone

Mathlib.CategoryTheory.Limits.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.isColimitConstCocone

Lean4

/-- When `J` is a connected category, the colimit of a
constant functor `J ⥤ C` with value `X : C` identifies to `X`. -/
def isColimitConstCocone : IsColimit (constCocone J X)
    where
  desc s := s.ι.app (Classical.arbitrary _)
  fac s
    j := by
    dsimp
    rw [id_comp]
    exact constant_of_preserves_morphisms _ (fun _ _ f ↦ by simpa using (s.w f).symm) _ _
  uniq s m hm := by simpa using hm (Classical.arbitrary _)

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

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

Разделы

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

Аффилиация

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