colimIsoLim

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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

Lean4

/-- If a category has biproducts of a shape `J`, its `colim` and `lim` functor on diagrams over `J`
are isomorphic. -/
@[simps!]
def colimIsoLim [HasBiproductsOfShape J C] : colim (J := Discrete J) (C := C) ≅ lim :=
  NatIso.ofComponents
    (fun F => (Sigma.isoColimit F).symm ≪≫ (biproduct.isoCoproduct _).symm ≪≫ biproduct.isoProduct _ ≪≫ Pi.isoLimit F)
    fun η =>
    colimit.hom_ext fun ⟨i⟩ =>
      limit.hom_ext fun ⟨j⟩ => by
        classical by_cases h : i = j <;> simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

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

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

Разделы

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

Аффилиация

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