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:
theorem HomOrthogonal.equiv_of_iso (o : HomOrthogonal s) {f : α → ι} {g : β → ι}
(i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) : ∃ e : α ≃ β, ∀ a, g (e a) = f a
This is preliminary to defining semisimple categories.
def
CategoryTheory.HomOrthogonal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
(s : ι → C)
:
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
- CategoryTheory.HomOrthogonal s = Pairwise fun (i j : ι) => Subsingleton (s i ⟶ s j)
Instances For
theorem
CategoryTheory.HomOrthogonal.eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(o : CategoryTheory.HomOrthogonal s)
{i : ι}
{j : ι}
(w : i ≠ j)
(f : s i ⟶ s j)
:
f = 0
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecomposition_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
(z : (⨁ fun (a : α) => s (f a)) ⟶ ⨁ fun (b : β) => s (g b))
(i : ι)
(j : ↑(g ⁻¹' {i}))
(k : ↑(f ⁻¹' {i}))
:
(CategoryTheory.HomOrthogonal.matrixDecomposition o) z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : s i = s (f ↑k)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j)
(CategoryTheory.eqToHom (_ : s (g ↑j) = s i)))
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
(z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
:
(CategoryTheory.HomOrthogonal.matrixDecomposition o).symm z = CategoryTheory.Limits.biproduct.matrix fun (j : α) (k : β) =>
if h : f j = g k then
CategoryTheory.CategoryStruct.comp
(z (f j) { val := k, property := (_ : k ∈ g ⁻¹' {f j}) } { val := j, property := (_ : j ∈ f ⁻¹' {f j}) })
(CategoryTheory.eqToHom (_ : s (f j) = s (g k)))
else 0
noncomputable def
CategoryTheory.HomOrthogonal.matrixDecomposition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
(z : (⨁ fun (a : α) => s ((fun (a : α) => f a) a)) ⟶ ⨁ fun (b : β) => s ((fun (b : β) => g b) b))
(i : ι)
(j : ↑((fun (b : β) => g b) ⁻¹' {i}))
(k : ↑((fun (a : α) => f a) ⁻¹' {i}))
:
(CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv o) z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : s i = s (f ↑k)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j)
(CategoryTheory.eqToHom (_ : s (g ↑j) = s i)))
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
(z : (i : ι) → Matrix (↑((fun (b : β) => g b) ⁻¹' {i})) (↑((fun (a : α) => f a) ⁻¹' {i})) (CategoryTheory.End (s i)))
:
(AddEquiv.symm (CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv o)) z = CategoryTheory.Limits.biproduct.matrix fun (j : α) (k : β) =>
if h : f j = g k then
CategoryTheory.CategoryStruct.comp
(z (f j) { val := k, property := (_ : k ∈ (fun (b : β) => g b) ⁻¹' {f j}) }
{ val := j, property := (_ : j ∈ (fun (a : α) => f a) ⁻¹' {f j}) })
(CategoryTheory.eqToHom (_ : s (f j) = s (g k)))
else 0
noncomputable def
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
:
HomOrthogonal.matrixDecomposition as an additive equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecomposition_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
[Fintype α]
{f : α → ι}
(i : ι)
:
(CategoryTheory.HomOrthogonal.matrixDecomposition o) (CategoryTheory.CategoryStruct.id (⨁ fun (a : α) => s (f a))) i = 1
theorem
CategoryTheory.HomOrthogonal.matrixDecomposition_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
{γ : Type}
[Fintype α]
[Fintype β]
[Fintype γ]
{f : α → ι}
{g : β → ι}
{h : γ → ι}
(z : (⨁ fun (a : α) => s (f a)) ⟶ ⨁ fun (b : β) => s (g b))
(w : (⨁ fun (b : β) => s (g b)) ⟶ ⨁ fun (c : γ) => s (h c))
(i : ι)
:
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{R : Type u_2}
[Semiring R]
[CategoryTheory.Linear R C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
:
∀ (a : (⨁ fun (a : α) => s (f a)) ⟶ ⨁ fun (b : β) => s (g b)) (i : ι),
(CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv o) a i = (CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv o).toEquiv.toFun a i
@[simp]
theorem
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{R : Type u_2}
[Semiring R]
[CategoryTheory.Linear R C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
:
∀ (a : (i : ι) → Matrix (↑((fun (b : β) => g b) ⁻¹' {i})) (↑((fun (a : α) => f a) ⁻¹' {i})) (CategoryTheory.End (s i))),
(LinearEquiv.symm (CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv o)) a = (CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv o).toEquiv.invFun a
noncomputable def
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{R : Type u_2}
[Semiring R]
[CategoryTheory.Linear R C]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
:
HomOrthogonal.MatrixDecomposition as an R-linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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).
theorem
CategoryTheory.HomOrthogonal.equiv_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_1}
{s : ι → C}
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))]
(o : CategoryTheory.HomOrthogonal s)
{α : Type}
{β : Type}
[Fintype α]
[Fintype β]
{f : α → ι}
{g : β → ι}
(i : (⨁ fun (a : α) => s (f a)) ≅ ⨁ fun (b : β) => s (g b))
:
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.