Commit 2020-07-01 10:05 8ba7595a

feat(category/preadditive): properties of preadditive biproducts (#3245)

Basic facts about morphisms between biproducts in preadditive categories.

• In any category (with zero morphisms), if biprod.map f g is an isomorphism, then both f and g are isomorphisms. The remaining lemmas hold in any preadditive category.
• If f is a morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct isomorphisms L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂ and R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂ so that L.hom ≫ g ≫ R.hom is diagonal (with X₁ ⟶ Y₁ component still f), via Gaussian elimination.
• As a corollary of the previous two facts, if we have an isomorphism X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, we can construct an isomorphism X₂ ≅ Y₂.
• If f : W ⊞ X ⟶ Y ⊞ Z is an isomorphism, either 𝟙 W = 0, or at least one of the component maps W ⟶ Y and W ⟶ Z is nonzero.
• If f : ⨁ S ⟶ ⨁ T is an isomorphism, then every column (corresponding to a nonzero summand in the domain) has some nonzero matrix entry. This PR is preliminary to some work on semisimple categories.