mathlib documentation

category_theory.limits.shapes.biproducts

Biproducts and binary biproducts

We introduce the notion of (finite) biproducts and binary biproducts.

These are slightly unusual relative to the other shapes in the library, as they are simultaneously limits and colimits. (Zero objects are similar; they are "biterminal".)

We treat first the case of a general category with zero morphisms, and subsequently the case of a preadditive category.

In a category with zero morphisms, we model the (binary) biproduct of P Q : C using a binary_bicone, which has a cone point X, and morphisms fst : X ⟶ P, snd : X ⟶ Q, inl : P ⟶ X and inr : X ⟶ Q, such that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q. Such a binary_bicone is a biproduct if the cone is a limit cone, and the cocone is a colimit cocone.

In a preadditive category,

For biproducts indexed by a fintype J, a bicone again consists of a cone point X and morphisms π j : X ⟶ F j and ι j : F j ⟶ X for each j, such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

In a preadditive category,

Notation

As is already taken for the sum of types, we introduce the notation X ⊞ Y for a binary biproduct. We introduce ⨁ f for the indexed biproduct.

@[nolint]
structure category_theory.limits.bicone {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
(J → C)Type (max u v)

A c : bicone F is:

  • an object c.X and
  • morphisms π j : X ⟶ F j and ι j : F j ⟶ X for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
@[simp]

@[simp]
theorem category_theory.limits.bicone_ι_π_ne {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {F : J → C} (B : category_theory.limits.bicone F) {j j' : J} :
j j'B.ι j B.π j' = 0

@[nolint]
structure category_theory.limits.limit_bicone {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
(J → C)Type (max u v)

A bicone over F : J → C, which is both a limit cone and a colimit cocone.

@[class]

has_biproduct F expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram F.

Instances

Use the axiom of choice to extract explicit biproduct_data F from has_biproduct F.

Equations
@[class]

C has biproducts of shape J if we have a limit and a colimit, with the same cone points, of every function F : J → C.

Instances
@[class]

has_finite_biproducts C represents a choice of biproduct for every family of objects in C indexed by a finite type with decidable equality.

Instances

biproduct f computes the biproduct of a family of elements f. (It is defined as an abbreviation for limit (discrete.functor f), so for most facts about biproduct f, you will just use general facts about limits and colimits.)

The projection onto a summand of a biproduct.

The inclusion into a summand of a biproduct.

def category_theory.limits.biproduct.lift {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {f : J → C} [category_theory.limits.has_biproduct f] {P : C} :
(Π (b : J), P f b)(P f)

Given a collection of maps into the summands, we obtain a map into the biproduct.

def category_theory.limits.biproduct.desc {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {f : J → C} [category_theory.limits.has_biproduct f] {P : C} :
(Π (b : J), f b P)( f P)

Given a collection of maps out of the summands, we obtain a map out of the biproduct.

@[simp]

Given a collection of maps between corresponding summands of a pair of biproducts indexed by the same type, we obtain a map between the biproducts.

An alternative to biproduct.map constructed via colimits. This construction only exists in order to show it is equal to biproduct.map.

@[nolint]

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

If the cone obtained from a bicone over pair X Y is a limit cone, so is the cone obtained by converting that bicone to a binary_bicone, then to a cone.

Equations

If the cocone obtained from a bicone over pair X Y is a colimit cocone, so is the cocone obtained by converting that bicone to a binary_bicone, then to a cocone.

Equations
@[nolint]

A bicone over P Q : C, which is both a limit cone and a colimit cocone.

@[class]

has_binary_biproduct P Q expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q.

Instances
@[class]

has_binary_biproducts C represents the existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.

A category with finite biproducts has binary biproducts.

This is not an instance as typically in concrete categories there will be an alternative construction with nicer definitional properties.

An arbitrary choice of biproduct of a pair of objects.

The projection onto the first summand of a binary biproduct.

The projection onto the second summand of a binary biproduct.

The inclusion into the first summand of a binary biproduct.

The inclusion into the second summand of a binary biproduct.

Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.

Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.

Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.

An alternative to biprod.map constructed via colimits. This construction only exists in order to show it is equal to biprod.map.

Given a pair of isomorphisms between the summands of a pair of binary biproducts, we obtain an isomorphism between the binary biproducts.

Equations

In a preadditive category, we can construct a biproduct for f : J → C from any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

In a preadditive category, if the product over f : J → C exists, then the biproduct over f exists.

In a preadditive category, if the coproduct over f : J → C exists, then the biproduct over f exists.

@[simp]

In any preadditive category, any biproduct satsifies ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)

@[simp]
theorem category_theory.limits.biproduct.lift_desc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type v} [decidable_eq J] [fintype J] {f : J → C} [category_theory.limits.has_biproduct f] {T U : C} {g : Π (j : J), T f j} {h : Π (j : J), f j U} :

@[simp]
theorem category_theory.limits.biproduct.lift_desc_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type v} [decidable_eq J] [fintype J] {f : J → C} [category_theory.limits.has_biproduct f] {T U : C} {g : Π (j : J), T f j} {h : Π (j : J), f j U} {X' : C} (f' : U X') :

In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

In a preadditive category, if the product of X and Y exists, then the binary biproduct of X and Y exists.

In a preadditive category, if the coproduct of X and Y exists, then the binary biproduct of X and Y exists.

@[simp]

In any preadditive category, any binary biproduct satsifies biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).

@[simp]
theorem category_theory.limits.biprod.lift_desc_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {T U : C} {f : T X} {g : T Y} {h : X U} {i : Y U} {X' : C} (f' : U X') :