English
Let C be a category with finite coproducts and pullbacks along inclusions. Then finitary extensivity of C is equivalent to a van Kampen property for a fixed binary copair (c0) consisting of a terminal object T. In other words, C is finitary extensive iff c0 is a van Kampen colimit.
Русский
Пусть C имеет конечные копродукты и вытягивания вдоль включений. Тогда конечная расширяемость C эквивалентна свойству ван Кампена для заданного двунасоединенного копроизведения c0, состоящего из терминального объекта T. Другими словами, C является конечной расширяемой тогда и только тогда c0 является колимитом ван Кампена.
LaTeX
$$$FinitaryExtensive\; C \quad\iff\quad IsVanKampenColimit\; c_0$$$
Lean4
theorem finitaryExtensive_iff_of_isTerminal (C : Type u) [Category.{v} C] [HasFiniteCoproducts C]
[HasPullbacksOfInclusions C] (T : C) (HT : IsTerminal T) (c₀ : BinaryCofan T T) (hc₀ : IsColimit c₀) :
FinitaryExtensive C ↔ IsVanKampenColimit c₀ :=
by
refine ⟨fun H => H.van_kampen' c₀ hc₀, fun H => ?_⟩
constructor
simp_rw [BinaryCofan.isVanKampen_iff] at H ⊢
intro X Y c hc X' Y' c' αX αY f hX hY
obtain ⟨d, hd, hd'⟩ := Limits.BinaryCofan.IsColimit.desc' hc (HT.from _ ≫ c₀.inl) (HT.from _ ≫ c₀.inr)
rw [H c' (αX ≫ HT.from _) (αY ≫ HT.from _) (f ≫ d) (by rw [← reassoc_of% hX, hd, Category.assoc])
(by rw [← reassoc_of% hY, hd', Category.assoc])]
obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩
rw [hl.paste_vert_iff hX.symm, hr.paste_vert_iff hY.symm]
