isLimitConstCone

Mathlib.CategoryTheory.Limits.Connected

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

Lean4

/-- When `J` is a connected category, the limit of a
constant functor `J ⥤ C` with value `X : C` identifies to `X`. -/
def isLimitConstCone : IsLimit (constCone J X)
    where
  lift s := s.π.app (Classical.arbitrary _)
  fac s
    j := by
    dsimp
    rw [comp_id]
    exact constant_of_preserves_morphisms _ (fun _ _ f ↦ by simpa using s.w f) _ _
  uniq s m hm := by simpa using hm (Classical.arbitrary _)

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

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

Разделы

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

Аффилиация

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