mathlib

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

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>