English
For any finite index set n, a finite coproduct of a diagram F:Discrete(n)→C is universal with respect to colimits in C when C is finitary pre-extensive.
Русский
Для любого конечного множества индексов n копроизведение диаграммы F: Discrete(n) → C является универсальным по отношению к колимитам в C, если C является конечнопредрасширенной.
LaTeX
$$$IsUniversalColimit\; c$ for finite coproducts in a finitaryPreExtensive setting.$$
Lean4
theorem isUniversal_finiteCoproducts_Fin [FinitaryPreExtensive C] {n : ℕ} {F : Discrete (Fin n) ⥤ C} {c : Cocone F}
(hc : IsColimit c) : IsUniversalColimit 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).isUniversal
| succ n
IH =>
refine
IsUniversalColimit.of_iso
(@isUniversalColimit_extendCofan _ _ _ _ _ _ (IH _ (coproductIsCoproduct _))
(FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
· dsimp
infer_instance
