Hom orthogonal families. #
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.
A family of objects is "hom orthogonal" if there is at most one morphism between distinct objects.
(In a category with zero morphisms, that must be the zero morphism.)
Equations
- category_theory.hom_orthogonal s = ∀ (i j : ι), i ≠ j → subsingleton (s i ⟶ s j)
Morphisms between two direct sums over a hom orthogonal family s : ι → C
are equivalent to block diagonal matrices,
with blocks indexed by ι
,
and matrix entries in i
-th block living in the endomorphisms of s i
.
Equations
- o.matrix_decomposition = {to_fun := λ (z : (⨁ λ (a : α), s (f a)) ⟶ ⨁ λ (b : β), s (g b)) (i : ι) (j : ↥(g ⁻¹' {i})) (k : ↥(f ⁻¹' {i})), category_theory.eq_to_hom _ ≫ category_theory.limits.biproduct.components z ↑k ↑j ≫ category_theory.eq_to_hom _, inv_fun := λ (z : Π (i : ι), matrix ↥(g ⁻¹' {i}) ↥(f ⁻¹' {i}) (category_theory.End (s i))), category_theory.limits.biproduct.matrix (λ (j : α) (k : β), dite (f j = g k) (λ (h : f j = g k), z (f j) ⟨k, _⟩ ⟨j, _⟩ ≫ category_theory.eq_to_hom _) (λ (h : ¬f j = g k), 0)), left_inv := _, right_inv := _}
hom_orthogonal.matrix_decomposition
as an additive equivalence.
Equations
- o.matrix_decomposition_add_equiv = {to_fun := o.matrix_decomposition.to_fun, inv_fun := o.matrix_decomposition.inv_fun, left_inv := _, right_inv := _, map_add' := _}
hom_orthogonal.matrix_decomposition
as an R
-linear equivalence.
Equations
- o.matrix_decomposition_linear_equiv = {to_fun := o.matrix_decomposition_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := o.matrix_decomposition_add_equiv.inv_fun, left_inv := _, right_inv := _}
The hypothesis that End (s i)
has invariant basis number is automatically satisfied
if s i
is simple (as then End (s i)
is a division ring).
Given a hom orthogonal family s : ι → C
for which each End (s i)
is a ring with invariant basis number (e.g. if each s i
is simple),
if two direct sums over s
are isomorphic, then they have the same multiplicities.