Commit 2022-05-24 03:06 179ae9e8
View on Github →feat(category_theory/preadditive): hom orthogonal families (#13871)
A family of objects in a category with zero morphisms is "hom orthogonal" if the only
morphism between distinct objects is the zero morphism.
We show that in any category with zero morphisms and finite biproducts,
a morphism between biproducts drawn from a hom orthogonal family s : ι → C
can be decomposed into a block diagonal matrix with entries in the endomorphism rings of the s i.
When the category is preadditive, this decomposition is an additive equivalence,
and intertwines composition and matrix multiplication.
When the category is R-linear, the decomposition is an R-linear equivalence.
If every object in the hom orthogonal family has an endomorphism ring with invariant basis number
(e.g. if each object in the family is simple, so its endomorphism ring is a division ring,
or otherwise if each endomorphism ring is commutative),
then decompositions of an object as a biproduct of the family have uniquely defined multiplicities.
We state this as:
lemma hom_orthogonal.equiv_of_iso (o : hom_orthogonal s) {f : α → ι} {g : β → ι}
(i : ⨁ (λ a, s (f a)) ≅ ⨁ (λ b, s (g b))) : ∃ e : α ≃ β, ∀ a, g (e a) = f a
This is preliminary to defining semisimple categories.