# mathlibdocumentation

category_theory.limits.preserves.shapes.biproducts

# Preservation of biproducts #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
@[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₂)

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 :

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₂)
• preserves : Π {b : ,

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]
@[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]
@[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]
@[protected, instance]
@[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.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) =