mathlib documentation

category_theory.preadditive.hom_orthogonal

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.

def category_theory.hom_orthogonal {C : Type u} [category_theory.category C] {ι : Type u_1} (s : ι → C) :
Prop

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
theorem category_theory.hom_orthogonal.eq_zero {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.limits.has_zero_morphisms C] (o : category_theory.hom_orthogonal s) {i j : ι} (w : i j) (f : s i s j) :
f = 0
noncomputable def category_theory.hom_orthogonal.matrix_decomposition {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} :
(( λ (a : α), s (f a)) λ (b : β), s (g b)) Π (i : ι), matrix (g ⁻¹' {i}) (f ⁻¹' {i}) (category_theory.End (s i))

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
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (z : ( λ (a : α), s (f a)) λ (b : β), s (g b)) (i : ι) (j : (g ⁻¹' {i})) (k : (f ⁻¹' {i})) :
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_symm_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (z : Π (i : ι), matrix (g ⁻¹' {i}) (f ⁻¹' {i}) (category_theory.End (s i))) :
(o.matrix_decomposition.symm) z = 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))
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_add_equiv_symm_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (ᾰ : Π (i : ι), matrix ((λ (b : β), g b) ⁻¹' {i}) ((λ (a : α), f a) ⁻¹' {i}) (category_theory.End (s i))) :
noncomputable def category_theory.hom_orthogonal.matrix_decomposition_add_equiv {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} :
(( λ (a : α), s (f a)) λ (b : β), s (g b)) ≃+ Π (i : ι), matrix (g ⁻¹' {i}) (f ⁻¹' {i}) (category_theory.End (s i))

hom_orthogonal.matrix_decomposition as an additive equivalence.

Equations
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_add_equiv_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (ᾰ : ( λ (a : α), s (f a)) λ (b : β), s (g b)) (i : ι) :
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_id {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α : Type} [fintype α] {f : α → ι} (i : ι) :
(o.matrix_decomposition) (𝟙 ( λ (a : α), s (f a))) i = 1
theorem category_theory.hom_orthogonal.matrix_decomposition_comp {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] (o : category_theory.hom_orthogonal s) {α β γ : Type} [fintype α] [fintype β] [fintype γ] {f : α → ι} {g : β → ι} {h : γ → ι} (z : ( λ (a : α), s (f a)) λ (b : β), s (g b)) (w : ( λ (b : β), s (g b)) λ (c : γ), s (h c)) (i : ι) :
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_linear_equiv_symm_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] {R : Type u_2} [semiring R] [category_theory.linear R C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (ᾰ : Π (i : ι), matrix ((λ (b : β), g b) ⁻¹' {i}) ((λ (a : α), f a) ⁻¹' {i}) (category_theory.End (s i))) :
noncomputable def category_theory.hom_orthogonal.matrix_decomposition_linear_equiv {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] {R : Type u_2} [semiring R] [category_theory.linear R C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} :
(( λ (a : α), s (f a)) λ (b : β), s (g b)) ≃ₗ[R] Π (i : ι), matrix (g ⁻¹' {i}) (f ⁻¹' {i}) (category_theory.End (s i))

hom_orthogonal.matrix_decomposition as an R-linear equivalence.

Equations
@[simp]
theorem category_theory.hom_orthogonal.matrix_decomposition_linear_equiv_apply {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] {R : Type u_2} [semiring R] [category_theory.linear R C] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (ᾰ : ( λ (a : α), s (f a)) λ (b : β), s (g b)) (i : ι) :

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 category_theory.hom_orthogonal.equiv_of_iso {C : Type u} [category_theory.category C] {ι : Type u_1} {s : ι → C} [category_theory.preadditive C] [category_theory.limits.has_finite_biproducts C] [∀ (i : ι), invariant_basis_number (category_theory.End (s i))] (o : category_theory.hom_orthogonal s) {α β : Type} [fintype α] [fintype β] {f : α → ι} {g : β → ι} (i : ( λ (a : α), s (f a)) λ (b : β), s (g b)) :
∃ (e : α β), ∀ (a : α), g (e a) = f a

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.