English
Finite van Kampen colimits characterize finitary extensive categories; finite discrete indexings suffice to verify the van Kampen property.
Русский
Конечные колимитные ван Кампена характеризуют конечную расширяемость; для проверки достаточно конечной дискретной индексации.
LaTeX
$$$IsVanKampenColimit\; c$ for finite discrete indexings$$
Lean4
theorem isVanKampen_finiteCoproducts_Fin [FinitaryExtensive C] {n : ℕ} {F : Discrete (Fin n) ⥤ C} {c : Cocone F}
(hc : IsColimit c) : IsVanKampenColimit c :=
by
let f : Fin n → C := F.obj ∘ Discrete.mk
have : F = Discrete.functor f := Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
clear_value f
subst this
induction n with
| zero => exact isVanKampenColimit_of_isEmpty _ hc
| succ n
IH =>
apply
IsVanKampenColimit.of_iso _
((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
· apply IH
exact coproductIsCoproduct _
· apply FinitaryExtensive.van_kampen'
exact coprodIsCoprod _ _
· dsimp
infer_instance
