Lean4
/-- The `Bicone` used in order to obtain the existence of
the biproduct of a functor `J ⥤ Karoubi C` when the category `C` is additive. -/
@[simps]
def bicone [HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → Karoubi C) : Bicone F
where
pt :=
{ X := biproduct fun j => (F j).X
p := biproduct.map fun j => (F j).p
idem := by
ext
simp only [assoc, biproduct.map_π, biproduct.map_π_assoc, idem] }
π
j :=
{ f := (biproduct.map fun j => (F j).p) ≫ Bicone.π _ j
comm := by simp only [assoc, biproduct.bicone_π, biproduct.map_π, biproduct.map_π_assoc, (F j).idem] }
ι
j :=
{ f := biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p
comm := by simp only [biproduct.ι_map, assoc, idem_assoc] }
ι_π j
j' := by
split_ifs with h
· subst h
simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl, id_f, hom_ext_iff, comp_f, assoc,
bicone_ι_π_self_assoc, idem]
· dsimp
simp only [biproduct.ι_map, biproduct.map_π, hom_ext_iff, comp_f, assoc, biproduct.ι_π_ne_assoc _ h, zero_comp,
comp_zero]
