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

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

The image of a bicone under a functor.

Equations
  • F.mapBicone b = { pt := F.obj b.pt, π := fun (j : J) => F.map (b j), ι := fun (j : J) => F.map (b j), ι_π := }
Instances For
    theorem CategoryTheory.Functor.mapBicone_whisker {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {K : Type w₂} {g : K J} {f : JC} (c : CategoryTheory.Limits.Bicone f) :
    F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g

    The image of a binary bicone under a functor.

    Equations
    Instances For
      class CategoryTheory.Limits.PreservesBiproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁} (f : JC) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
      Type (max (max (max (max u₁ u₂) v₁) v₂) w₁)

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

      • preserves : {b : CategoryTheory.Limits.Bicone f} → b.IsBilimit(F.mapBicone b).IsBilimit

        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.

          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

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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.

                  • preserves : {b : CategoryTheory.Limits.BinaryBicone X Y} → b.IsBilimit(F.mapBinaryBicone b).IsBilimit

                    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.

                      Instances

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          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.

                              @[simp]

                              biproduct_comparison F f is a split epimorphism.

                              Equations
                              • F.splitEpiBiproductComparison f = { section_ := F.biproductComparison' f, id := }
                              Instances For
                                @[simp]

                                biproduct_comparison' F f is a split monomorphism.

                                Equations
                                • F.splitMonoBiproductComparison' f = { retraction := F.biproductComparison f, id := }
                                Instances For

                                  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.

                                        biprodComparison F X Y is a split epi.

                                        Equations
                                        • F.splitEpiBiprodComparison X Y = { section_ := F.biprodComparison' X Y, id := }
                                        Instances For

                                          biprodComparison' F X Y is a split mono.

                                          Equations
                                          • F.splitMonoBiprodComparison' X Y = { retraction := F.biprodComparison X Y, id := }
                                          Instances For

                                            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.Functor.mapBiprod_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] :
                                              (F.mapBiprod X Y).hom = CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)
                                              theorem CategoryTheory.Functor.mapBiprod_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] :
                                              (F.mapBiprod X Y).inv = CategoryTheory.Limits.biprod.desc (F.map CategoryTheory.Limits.biprod.inl) (F.map CategoryTheory.Limits.biprod.inr)