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

The image of a bicone under a functor.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Functor.mapBicone_ι {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : JC} (b : Limits.Bicone f) (j : J) :
    (F.mapBicone b).ι j = F.map (b.ι j)
    @[simp]
    theorem CategoryTheory.Functor.mapBicone_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : JC} (b : Limits.Bicone f) (j : J) :
    (F.mapBicone b).π j = F.map (b.π j)

    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 f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

      Equations
      Instances For

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

        • preserves {f : JC} : PreservesBiproduct f F

          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 finite type.

          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.

            • preserves {J : Type w₁} : PreservesBiproductsOfShape J F

              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

              Preserving biproducts at a bigger universe level implies preserving biproducts at a smaller universe level.

              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 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.

                Equations
                Instances For

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

                  • preserves {X Y : C} : PreservesBinaryBiproduct X Y F

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

                  Instances

                    A functor that preserves biproducts of a pair preserves binary biproducts.

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

                    Equations
                    Instances For

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

                      Equations
                      Instances For
                        @[simp]

                        The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBiproduct_of_monoBiproductComparison.

                        biproduct_comparison F f is a split epimorphism.

                        Equations
                        Instances For

                          biproduct_comparison' F f is a split monomorphism.

                          Equations
                          Instances For
                            @[reducible, inline]

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

                            Equations
                            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.

                              Equations
                              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).

                                Equations
                                Instances For
                                  @[simp]

                                  The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBinaryBiproduct_of_monoBiprodComparison.

                                  @[reducible, inline]

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

                                  Equations
                                  Instances For
                                    theorem CategoryTheory.Limits.biproduct.map_lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : JC) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → W f j) :
                                    CategoryStruct.comp (F.map (lift g)) (F.mapBiproduct f).hom = lift fun (j : J) => F.map (g j)
                                    theorem CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : JC) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j W) :
                                    CategoryStruct.comp (F.mapBiproduct f).inv (F.map (desc g)) = desc fun (j : J) => F.map (g j)
                                    theorem CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : JC) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j W) :
                                    CategoryStruct.comp (F.mapBiproduct f).hom (desc fun (j : J) => F.map (g j)) = F.map (desc g)