English
If C has finite biproducts, then its Karoubi envelope Karoubi(C) also has finite biproducts.
Русский
Пусть C имеет конечные биобразные произведения; тогда оболочка Кароуби Karoubi(C) также имеет конечные биобразные произведения.
LaTeX
$$$\\operatorname{HasFiniteBiproducts}(C) \\Rightarrow \\operatorname{HasFiniteBiproducts}(\\operatorname{Karoubi}(C))$$$
Lean4
theorem karoubi_hasFiniteBiproducts [HasFiniteBiproducts C] : HasFiniteBiproducts (Karoubi C) :=
{
out := fun n =>
{
has_biproduct := fun F => by
apply hasBiproduct_of_total (Biproducts.bicone F)
simp only [hom_ext_iff]
refine biproduct.hom_ext' _ _ (fun j => ?_)
simp only [Biproducts.bicone_pt_X, sum_hom, comp_f, Biproducts.bicone_π_f, biproduct.bicone_π,
biproduct.map_π, Biproducts.bicone_ι_f, biproduct.ι_map, assoc, idem_assoc, id_f, Biproducts.bicone_pt_p,
comp_sum]
rw [Finset.sum_eq_single j]
· simp only [bicone_ι_π_self_assoc]
· intro b _ hb
simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
· intro hj
simp only [Finset.mem_univ, not_true] at hj } }
