isColimitPUnitCocone

Mathlib.CategoryTheory.Limits.IsConnected

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

Lean4

/-- If `C` is connected, the cocone on `constPUnitFunctor` with cone point `PUnit` is a colimit
cocone. -/
noncomputable def isColimitPUnitCocone [IsConnected C] : IsColimit (pUnitCocone.{w} C)
    where
  desc s := s.ι.app Classical.ofNonempty
  fac s
    j := by
    ext ⟨⟩
    apply constant_of_preserves_morphisms (s.ι.app · PUnit.unit)
    intro X Y f
    exact congrFun (s.ι.naturality f).symm PUnit.unit
  uniq s m
    h := by
    ext ⟨⟩
    simp [← h Classical.ofNonempty]

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

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

Разделы

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

Аффилиация

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