# mathlibdocumentation

category_theory.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 preserves_biproduct and preserves_binary_biproduct. We then

• show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
• construct the comparison morphisms between the image of a biproduct and the biproduct of the images and show that the biproduct is preserved if one of them is an isomorphism,
• give the canonical isomorphism between the image of a biproduct and the biproduct of the images in case that the biproduct is preserved,
• show that in a preadditive category, a functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.
@[simp]
theorem category_theory.functor.map_bicone_X {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} {f : J → C}  :
(F.map_bicone b).X = F.obj b.X
@[simp]
theorem category_theory.functor.map_bicone_π {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} {f : J → C} (j : J) :
(F.map_bicone b).π j = F.map (b.π j)
def category_theory.functor.map_bicone {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} {f : J → C}  :

The image of a bicone under a functor.

Equations
@[simp]
theorem category_theory.functor.map_bicone_ι {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} {f : J → C} (j : J) :
(F.map_bicone b).ι j = F.map (b.ι j)
theorem category_theory.functor.map_bicone_whisker {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} {K : Type w₂} {g : K J} {f : J → C}  :
@[simp]
theorem category_theory.functor.map_binary_bicone_X {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
@[simp]
theorem category_theory.functor.map_binary_bicone_inl {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
@[simp]
theorem category_theory.functor.map_binary_bicone_snd {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
@[simp]
theorem category_theory.functor.map_binary_bicone_fst {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
def category_theory.functor.map_binary_bicone {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
(F.obj Y)

The image of a binary bicone under a functor.

Equations
@[simp]
theorem category_theory.functor.map_binary_bicone_inr {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :
@[class]
structure category_theory.limits.preserves_biproduct {C : Type u₁} {D : Type u₂} {J : Type w₁} (f : J → C) (F : C D)  :
Type (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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproduct
• category_theory.limits.preserves_biproduct.has_sizeof_inst
def category_theory.limits.is_bilimit_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w₁} {f : J → C} (F : C D) (hb : b.is_bilimit) :

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

Equations
@[class]
structure category_theory.limits.preserves_biproducts_of_shape {C : Type u₁} {D : Type u₂} (J : Type w₁) (F : C D)  :
Type (max u₁ u₂ v₁ v₂ w₁)
• preserves : Π {f : J → C},

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

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproducts_of_shape
• category_theory.limits.preserves_biproducts_of_shape.has_sizeof_inst
@[class]
structure category_theory.limits.preserves_finite_biproducts {C : Type u₁} {D : Type u₂} (F : C D)  :
Type (max 1 u₁ u₂ v₁ v₂)
• preserves : Π {J : Type} [_inst_5_1 : fintype J],

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

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_finite_biproducts
• category_theory.limits.preserves_finite_biproducts.has_sizeof_inst
@[class]
structure category_theory.limits.preserves_biproducts {C : Type u₁} {D : Type u₂} (F : C D)  :
Type (max u₁ u₂ v₁ v₂ (w₁+1))
• preserves : Π {J : Type ?},

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 for category_theory.limits.preserves_biproducts
• category_theory.limits.preserves_biproducts.has_sizeof_inst

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

Equations
@[protected, instance]
Equations
@[class]
structure category_theory.limits.preserves_binary_biproduct {C : Type u₁} {D : Type u₂} (X Y : C) (F : C D)  :
Type (max u₁ u₂ v₁ v₂)

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 of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_binary_biproduct
• category_theory.limits.preserves_binary_biproduct.has_sizeof_inst
def category_theory.limits.is_binary_bilimit_of_preserves {C : Type u₁} {D : Type u₂} {X Y : C} (F : C D) (hb : b.is_bilimit) :

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
@[class]
structure category_theory.limits.preserves_binary_biproducts {C : Type u₁} {D : Type u₂} (F : C D)  :
Type (max u₁ u₂ v₁ v₂)
• preserves : (Π {X Y : C}, . "apply_instance"

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

Instances for category_theory.limits.preserves_binary_biproducts
• category_theory.limits.preserves_binary_biproducts.has_sizeof_inst

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

Equations

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

Equations
noncomputable def category_theory.functor.biproduct_comparison {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
F.obj ( f) F.obj f

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

Equations
Instances for category_theory.functor.biproduct_comparison
@[simp]
theorem category_theory.functor.biproduct_comparison_π {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C) (j : J) :
=
@[simp]
theorem category_theory.functor.biproduct_comparison_π_assoc {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C) (j : J) {X' : D} (f' : (F.obj f) j X') :
f' = f'
noncomputable def category_theory.functor.biproduct_comparison' {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
F.obj f F.obj ( f)

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

Equations
Instances for category_theory.functor.biproduct_comparison'
@[simp]
theorem category_theory.functor.ι_biproduct_comparison' {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C) (j : J) :
=
@[simp]
theorem category_theory.functor.ι_biproduct_comparison'_assoc {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C) (j : J) {X' : D} (f' : F.obj ( f) X') :
f' = f'
@[simp]
theorem category_theory.functor.biproduct_comparison'_comp_biproduct_comparison_assoc {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C) {X' : D} (f' : F.obj f X') :
f' = f'
@[simp]
theorem category_theory.functor.biproduct_comparison'_comp_biproduct_comparison {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
= 𝟙 ( F.obj f)

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

noncomputable def category_theory.functor.split_epi_biproduct_comparison {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :

biproduct_comparison F f is a split epimorphism.

Equations
@[simp]
theorem category_theory.functor.split_epi_biproduct_comparison_section_ {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
@[protected, instance]
def category_theory.functor.biproduct_comparison.category_theory.is_split_epi {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
noncomputable def category_theory.functor.split_mono_biproduct_comparison' {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :

biproduct_comparison' F f is a split monomorphism.

Equations
@[simp]
theorem category_theory.functor.split_mono_biproduct_comparison'_retraction {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
@[protected, instance]
def category_theory.functor.biproduct_comparison'.category_theory.is_split_mono {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
@[protected, instance]
def category_theory.functor.has_biproduct_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
@[simp]
noncomputable def category_theory.functor.map_biproduct {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
F.obj ( f) F.obj f

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

Equations
theorem category_theory.functor.map_biproduct_hom {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
theorem category_theory.functor.map_biproduct_inv {C : Type u₁} {D : Type u₂} {J : Type w₁} (F : C D) (f : J → C)  :
noncomputable def category_theory.functor.biprod_comparison {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
F.obj (X Y) F.obj X F.obj Y

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 category_theory.functor.biprod_comparison
@[simp]
theorem category_theory.functor.biprod_comparison_fst_assoc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] {X' : D} (f' : F.obj X X') :
@[simp]
theorem category_theory.functor.biprod_comparison_fst {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
@[simp]
theorem category_theory.functor.biprod_comparison_snd_assoc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] {X' : D} (f' : F.obj Y X') :
@[simp]
theorem category_theory.functor.biprod_comparison_snd {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
noncomputable def category_theory.functor.biprod_comparison' {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
F.obj X F.obj Y F.obj (X Y)

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 category_theory.functor.biprod_comparison'
@[simp]
theorem category_theory.functor.inl_biprod_comparison'_assoc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] {X' : D} (f' : F.obj (X Y) X') :
@[simp]
theorem category_theory.functor.inl_biprod_comparison' {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
@[simp]
theorem category_theory.functor.inr_biprod_comparison' {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] :
@[simp]
theorem category_theory.functor.inr_biprod_comparison'_assoc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] {X' : D} (f' : F.obj (X Y) X') :
@[simp]
theorem category_theory.functor.biprod_comparison'_comp_biprod_comparison {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :
Y Y = 𝟙 (F.obj X F.obj Y)

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

@[simp]
theorem category_theory.functor.biprod_comparison'_comp_biprod_comparison_assoc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)] {X' : D} (f' : F.obj X F.obj Y X') :
Y Y f' = f'
@[simp]
theorem category_theory.functor.split_epi_biprod_comparison_section_ {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :
Y).section_ = Y
noncomputable def category_theory.functor.split_epi_biprod_comparison {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :

biprod_comparison F X Y is a split epi.

Equations
@[protected, instance]
def category_theory.functor.biprod_comparison.category_theory.is_split_epi {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :
@[simp]
theorem category_theory.functor.split_mono_biprod_comparison'_retraction {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :
= Y
noncomputable def category_theory.functor.split_mono_biprod_comparison' {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :

biprod_comparison' F X Y is a split mono.

Equations
@[protected, instance]
def category_theory.functor.biprod_comparison'.category_theory.is_split_mono {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) [ (F.obj Y)]  :
@[protected, instance]
def category_theory.functor.has_binary_biproduct_of_preserves {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C)  :
(F.obj Y)
@[simp]
noncomputable def category_theory.functor.map_biprod {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C)  :
F.obj (X Y) F.obj X F.obj Y

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

Equations
theorem category_theory.functor.map_biprod_hom {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C)  :
theorem category_theory.functor.map_biprod_inv {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C)  :
theorem category_theory.limits.biproduct.map_lift_map_biprod {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} (f : J → C) {W : C} (g : Π (j : J), W f j) :
theorem category_theory.limits.biproduct.map_biproduct_inv_map_desc {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} (f : J → C) {W : C} (g : Π (j : J), f j W) :
theorem category_theory.limits.biproduct.map_biproduct_hom_desc {C : Type u₁} {D : Type u₂} (F : C D) {J : Type w₁} (f : J → C) {W : C} (g : Π (j : J), f j W) :
theorem category_theory.limits.biprod.map_lift_map_biprod {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) {W : C} (f : W X) (g : W Y) :
(F.map_biprod X Y).hom = (F.map g)
theorem category_theory.limits.biprod.lift_map_biprod {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) {W : C} (f : W X) (g : W Y) :
(F.map g) (F.map_biprod X Y).inv =
theorem category_theory.limits.biprod.map_biprod_inv_map_desc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) {W : C} (f : X W) (g : Y W) :
(F.map_biprod X Y).inv = (F.map g)
theorem category_theory.limits.biprod.map_biprod_hom_desc {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) {W : C} (f : X W) (g : Y W) :
(F.map_biprod X Y).hom (F.map g) =
noncomputable def category_theory.limits.preserves_product_of_preserves_biproduct {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

Equations
noncomputable def category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J]  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

Equations
def category_theory.limits.preserves_biproduct_of_preserves_product {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

Equations
noncomputable def category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

If the (product-like) biproduct comparison for F and f is a monomorphism, then F preserves the biproduct of f. For the converse, see map_biproduct.

Equations
noncomputable def category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison' {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

If the (coproduct-like) biproduct comparison for F and f is an epimorphism, then F preserves the biproduct of F and f. For the converse, see map_biproduct.

Equations
def category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J]  :

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

Equations
noncomputable def category_theory.limits.preserves_coproduct_of_preserves_biproduct {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

Equations
noncomputable def category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J]  :

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

Equations
def category_theory.limits.preserves_biproduct_of_preserves_coproduct {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J] {f : J → C}  :

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

Equations
def category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape {C : Type u₁} {D : Type u₂} (F : C D) {J : Type} [fintype J]  :

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

Equations
def category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

Equations
def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

Equations
noncomputable def category_theory.limits.preserves_binary_biproduct_of_mono_biprod_comparison {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} [ (F.obj Y)] [category_theory.mono Y)] :

If the (product-like) biproduct comparison for F, X and Y is a monomorphism, then F preserves the biproduct of X and Y. For the converse, see map_biprod.

Equations
noncomputable def category_theory.limits.preserves_binary_biproduct_of_epi_biprod_comparison' {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} [ (F.obj Y)] [category_theory.epi Y)] :

If the (coproduct-like) biproduct comparison for F, X and Y is an epimorphism, then F preserves the biproduct of X and Y. For the converse, see map_biprod.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

Equations
def category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

Equations
def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C}  :

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

Equations

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

Equations