isVanKampenColimit — Mathlib

English

If C has strict initial objects and X is initial, then the empty cocone at X is a Van Kampen colimit.

Русский

Пусть у категории C есть строгие начальные объекты, и X является начальным; тогда пустой кокон над X является колимитом Ван-Кампена.

LaTeX

$$$[HasStrictInitialObjects(C)]\\; \\Rightarrow\\; \\bigl( \\IsInitial(X) \\Rightarrow \\IsVanKampenColimit(\\operatorname{asEmptyCocone}(X))\\bigr)$$$

Lean4

theorem isVanKampenColimit [HasStrictInitialObjects C] {X : C} (h : IsInitial X) :
    IsVanKampenColimit (asEmptyCocone X) := by
  intro F' c' α f hf hα
  have : F' = Functor.empty C := by apply Functor.hext <;> rintro ⟨⟨⟩⟩
  subst this
  haveI := h.isIso_to f
  refine ⟨by rintro _ ⟨⟨⟩⟩, fun _ => ⟨IsColimit.ofIsoColimit h (Cocones.ext (asIso f).symm <| by rintro ⟨⟨⟩⟩)⟩⟩

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