sigmaCofanIsColimit

Mathlib.Topology.Category.TopCat.Limits.Products

URI: https://scilib.ai/kg/mathlib#TopCat.sigmaCofanIsColimit

Lean4

/-- The constructed cofan is indeed a colimit -/
def sigmaCofanIsColimit {ι : Type v} (β : ι → TopCat.{max v u}) : IsColimit (sigmaCofan β)
    where
  desc
    S :=
    ofHom
      { toFun := fun (s : of (Σ i, β i)) => S.ι.app ⟨s.1⟩ s.2
        continuous_toFun := by continuity }
  uniq := by
    intro S m h
    ext ⟨i, x⟩
    simp only [← h]
    congr
  fac s
    j := by
    cases j
    cat_disch

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

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

Разделы

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

Аффилиация

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