Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Preservation of biproducts #

We define the image of a (binary) bicone under a functor that preserves zero morphisms and define classes PreservesBiproduct and PreservesBinaryBiproduct. We then

A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

Instances

    A functor F preserves biproducts of shape J if it preserves biproducts of f for every f : J → C.

    Instances

      A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a fintype.

      Instances
        • A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

        A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

        Instances

          A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

          Instances

            A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y for all X and Y.

            Instances

              As for products, any functor between categories with biproducts gives rise to a morphism F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f).

              Instances For

                As for coproducts, any functor between categories with biproducts gives rise to a morphism ⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)

                Instances For

                  If F preserves a biproduct, we get a definitionally nice isomorphism F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f).

                  Instances For

                    As for products, any functor between categories with binary biproducts gives rise to a morphism F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y.

                    Instances For

                      As for coproducts, any functor between categories with binary biproducts gives rise to a morphism F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y).

                      Instances For

                        If F preserves a binary biproduct, we get a definitionally nice isomorphism F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y.

                        Instances For