English
For a finite index J, a bilimit cone for a family f: J → C is characterized by a total equality: the sum over j of f.j followed by the iota_j equals the identity.
Русский
Для конечного индекса J билимитет для семейства f: J → C определяется равенством total: сумма по j из J элементов f.j ⋯ iota_j равна тождению.
LaTeX
$$∑_{j ∈ J} (b.π_j ≫ b.ι_j) = 𝟙_b.pt$$
Lean4
/-- In a preadditive category, we can construct a biproduct for `f : J → C` from
any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.
(That is, such a bicone is a limit cone and a colimit cocone.)
-/
def isBilimitOfTotal {f : J → C} (b : Bicone f) (total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt) : b.IsBilimit
where
isLimit :=
{ lift := fun s => ∑ j : J, s.π.app ⟨j⟩ ≫ b.ι j
uniq := fun s m h => by
rw [← Category.comp_id m]
dsimp
rw [← total, comp_sum]
apply Finset.sum_congr rfl
intro j _
have reassoced : m ≫ Bicone.π b j ≫ Bicone.ι b j = s.π.app ⟨j⟩ ≫ Bicone.ι b j := by
simpa using eq_whisker (h ⟨j⟩) _
rw [reassoced]
fac := fun s j => by
classical
cases j
simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
simp }
isColimit :=
{ desc := fun s => ∑ j : J, b.π j ≫ s.ι.app ⟨j⟩
uniq := fun s m h => by
rw [← Category.id_comp m]
dsimp
rw [← total, sum_comp]
apply Finset.sum_congr rfl
intro j _
simpa using b.π j ≫= h ⟨j⟩
fac := fun s j => by
classical
cases j
simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
simp }
