CategoryTheory.HomOrthogonal.equiv_of_iso

theorem CategoryTheory.HomOrthogonal.equiv_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_3 : ∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))], CategoryTheory.HomOrthogonal s → ∀ {α β : Type} [inst_4 : Finite α] [inst_5 : Finite β] {f : α → ι} {g : β → ι}, ((⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) → ∃ e, ∀ (a : α), g (e a) = f a

This theorem establishes a condition for isomorphisms between direct sums in category theory. Specifically, it states that if a family of objects `s : ι → C` in a category is "hom orthogonal" (there is at most one morphism between distinct objects), and each endomorphism ring `End (s i)` has an invariant basis number (for instance, each `s i` is simple), then if two direct sums over `s` are isomorphic, they must have the same multiplicities. In other words, there exists a function `e` such that for every element `a` of some type `α`, `g (e a) = f a`. This theorem is relevant in a category that supports addition ("preadditive") and has finite "biproducts" - a generalization of the concept of a direct sum and a direct product.

More concisely: If `s : ι → C` is a hom orthogonal family of objects in a preadditive category with finite biproducts, where each `s i` has an invariant basis number, then isomorphic direct sums over `s` have the same multiplicities.