Documentation

Mathlib.CategoryTheory.Preadditive.Biproducts

Basic facts about biproducts in preadditive categories. #

In (or between) preadditive categories,

There are connections between this material and the special case of the category whose morphisms are matrices over a ring, in particular the Schur complement (see Mathlib.LinearAlgebra.Matrix.SchurComplement). In particular, the declarations CategoryTheory.Biprod.isoElim, CategoryTheory.Biprod.gaussian and Matrix.invertibleOfFromBlocks₁₁Invertible are all closely related.

In a preadditive category, we can construct a biproduct for f : J → C from any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

Instances For

    In a preadditive category, we can construct a biproduct for f : J → C from any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.

    (That is, such a bicone is a limit cone and a colimit cocone.)

    In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.

    Instances For

      In a preadditive category, if the product over f : J → C exists, then the biproduct over f exists.

      In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

      Instances For

        In a preadditive category, if the coproduct over f : J → C exists, then the biproduct over f exists.

        @[simp]

        In any preadditive category, any biproduct satsifies ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)

        Reindex a categorical biproduct via an equivalence of the index types.

        Instances For

          In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.

          (That is, such a bicone is a limit cone and a colimit cocone.)

          Instances For

            In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.

            (That is, such a bicone is a limit cone and a colimit cocone.)

            In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.

            Instances For

              In a preadditive category, if the product of X and Y exists, then the binary biproduct of X and Y exists.

              In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.

              Instances For

                In a preadditive category, if the coproduct of X and Y exists, then the binary biproduct of X and Y exists.

                @[simp]
                theorem CategoryTheory.Limits.biprod.total {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] :
                CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr = CategoryTheory.CategoryStruct.id (X Y)

                In any preadditive category, any binary biproduct satsifies biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).

                theorem CategoryTheory.Limits.biprod.map_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W : C} {X : C} {Y : C} {Z : C} {f : W Y} {g : X Z} :
                CategoryTheory.Limits.biprod.map f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl) + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr)
                @[simp]

                Every split mono f with a cokernel induces a binary bicone with f as its inl and the cokernel map as its snd. We will show in is_bilimit_binary_bicone_of_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

                Instances For

                  The bicone constructed in binaryBiconeOfSplitMonoOfCokernel is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

                  Instances For

                    Every split epi f with a kernel induces a binary bicone with f as its snd and the kernel map as its inl. We will show in binary_bicone_of_is_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

                    Instances For
                      theorem CategoryTheory.Preadditive.ext {C : Type u} :
                      ∀ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C), CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroupx = y
                      theorem CategoryTheory.Preadditive.ext_iff {C : Type u} :
                      ∀ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C), x = y CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup
                      def CategoryTheory.Biprod.ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
                      X₁ X₂ Y₁ Y₂

                      The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.

                      Instances For
                        @[simp]
                        theorem CategoryTheory.Biprod.inl_ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
                        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryTheory.CategoryStruct.comp f₁₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp f₁₂ CategoryTheory.Limits.biprod.inr
                        @[simp]
                        theorem CategoryTheory.Biprod.inr_ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
                        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryTheory.CategoryStruct.comp f₂₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp f₂₂ CategoryTheory.Limits.biprod.inr
                        @[simp]
                        theorem CategoryTheory.Biprod.ofComponents_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₁ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₁
                        @[simp]
                        theorem CategoryTheory.Biprod.ofComponents_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₂ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₂
                        @[simp]
                        theorem CategoryTheory.Biprod.ofComponents_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f : X₁ X₂ Y₁ Y₂) :
                        CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) = f
                        @[simp]
                        theorem CategoryTheory.Biprod.ofComponents_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} {Z₁ : C} {Z₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) (g₁₁ : Y₁ Z₁) (g₁₂ : Y₁ Z₂) (g₂₁ : Y₂ Z₁) (g₂₂ : Y₂ Z₂) :

                        The unipotent upper triangular matrix

                        (1 r)
                        (0 1)
                        

                        as an isomorphism.

                        Instances For

                          The unipotent lower triangular matrix

                          (1 0)
                          (r 1)
                          

                          as an isomorphism.

                          Instances For
                            def CategoryTheory.Biprod.gaussian' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) [CategoryTheory.IsIso f₁₁] :
                            (L : X₁ X₂ X₁ X₂) ×' (R : Y₁ Y₂ Y₁ Y₂) ×' (g₂₂ : X₂ Y₂) ×' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) R.hom) = CategoryTheory.Limits.biprod.map f₁₁ g₂₂

                            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.

                            (This is the version of Biprod.gaussian written in terms of components.)

                            Instances For
                              def CategoryTheory.Biprod.gaussian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f : X₁ X₂ Y₁ Y₂) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))] :
                              (L : X₁ X₂ X₁ X₂) ×' (R : Y₁ Y₂ Y₁ Y₂) ×' (g₂₂ : X₂ Y₂) ×' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) g₂₂

                              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.

                              Instances For
                                def CategoryTheory.Biprod.isoElim' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) [CategoryTheory.IsIso f₁₁] [CategoryTheory.IsIso (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)] :
                                X₂ Y₂

                                If X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ via a two-by-two matrix whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct an isomorphism X₂ ≅ Y₂, via Gaussian elimination.

                                Instances For
                                  def CategoryTheory.Biprod.isoElim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f : X₁ X₂ Y₁ Y₂) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.Limits.biprod.fst))] :
                                  X₂ Y₂

                                  If f is an isomorphism X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct an isomorphism X₂ ≅ Y₂, via Gaussian elimination.

                                  Instances For
                                    theorem CategoryTheory.Biprod.column_nonzero_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W : C} {X : C} {Y : C} {Z : C} (f : W X Y Z) [CategoryTheory.IsIso f] :
                                    CategoryTheory.CategoryStruct.id W = 0 CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst) 0 CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd) 0

                                    If f : ⨁ S ⟶ ⨁ T is an isomorphism, and s is a non-trivial summand of the source, then there is some t in the target so that the s, t matrix entry of f is nonzero.

                                    Instances For