English
In a finitely extensive category, every colimit of a diagram F: Discrete WalkingPair ⥤ C is a van Kampen colimit.
Русский
В конечносильно-разложимой категории каждый предел-колимит для диаграммы F: Discrete WalkingPair ⥤ C является пределом Ван-Кампена.
LaTeX
$$$[\text{FinitaryExtensive}(C)]\; \forall F: \text{Discrete WalkingPair} \to C,\ \forall c: \text{Cocone } F,\ IsColimit(c) \Rightarrow IsVanKampenColimit(c)$$$
Lean4
theorem vanKampen [FinitaryExtensive C] {F : Discrete WalkingPair ⥤ C} (c : Cocone F) (hc : IsColimit c) :
IsVanKampenColimit c := by
let X := F.obj ⟨WalkingPair.left⟩
let Y := F.obj ⟨WalkingPair.right⟩
have : F = pair X Y := by
apply Functor.hext
· rintro ⟨⟨⟩⟩ <;> rfl
· rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X, Y]
clear_value X Y
subst this
exact FinitaryExtensive.van_kampen' c hc
