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.

Implementation #

Prior to #14046, has_finite_biproducts required a decidable_eq instance on the indexing type. As this had no pay-off (everything about limits is non-constructive in mathlib), and occasional cost (constructing decidability instances appropriate for constructions involving the indexing type), we made everything classical.

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

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.
Instances for category_theory.limits.bicone
  • category_theory.limits.bicone.has_sizeof_inst
@[simp]
theorem category_theory.limits.bicone_ι_π_self {J : Type w} {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) :
B.ι j B.π j = 𝟙 (F j)
@[simp]
theorem category_theory.limits.bicone_ι_π_self_assoc {J : Type w} {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) {X' : C} (f' : F j X') :
B.ι j B.π j f' = f'
@[simp]
theorem category_theory.limits.bicone_ι_π_ne {J : Type w} {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} (h : j j') :
B.ι j B.π j' = 0
@[simp]
theorem category_theory.limits.bicone_ι_π_ne_assoc {J : Type w} {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} (h : j j') {X' : C} (f' : F j' X') :
B.ι j B.π j' f' = 0 f'

We can turn any limit cone over a discrete collection of objects into a bicone.

Equations
theorem category_theory.limits.bicone.ι_of_is_limit {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {f : J → C} {t : category_theory.limits.bicone f} (ht : category_theory.limits.is_limit t.to_cone) (j : J) :
t.ι j = ht.lift (category_theory.limits.fan.mk (f j) (λ (j' : J), dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)))

We can turn any colimit cocone over a discrete collection of objects into a bicone.

Equations
theorem category_theory.limits.bicone.π_of_is_colimit {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {f : J → C} {t : category_theory.limits.bicone f} (ht : category_theory.limits.is_colimit t.to_cocone) (j : J) :
t.π j = ht.desc (category_theory.limits.cofan.mk (f j) (λ (j' : J), dite (j' = j) (λ (h : j' = j), category_theory.eq_to_hom _) (λ (h : ¬j' = j), 0)))
@[nolint]
structure category_theory.limits.bicone.is_bilimit {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {F : J → C} (B : category_theory.limits.bicone F) :
Type (max u v w)

Structure witnessing that a bicone is both a limit cone and a colimit cocone.

Instances for category_theory.limits.bicone.is_bilimit
theorem category_theory.limits.bicone.is_bilimit.ext {J : Type w} {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {F : J → C} {B : category_theory.limits.bicone F} (x y : B.is_bilimit) (h : x.is_limit = y.is_limit) (h_1 : x.is_colimit = y.is_colimit) :
x = y
@[simp]
theorem category_theory.limits.bicone.whisker_π {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {K : Type w'} {f : J → C} (c : category_theory.limits.bicone f) (g : K J) (k : K) :
(c.whisker g).π k = c.π (g k)
@[simp]
theorem category_theory.limits.bicone.whisker_X {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {K : Type w'} {f : J → C} (c : category_theory.limits.bicone f) (g : K J) :
(c.whisker g).X = c.X

Whisker a bicone with an equivalence between the indexing types.

Equations
@[simp]
theorem category_theory.limits.bicone.whisker_ι {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {K : Type w'} {f : J → C} (c : category_theory.limits.bicone f) (g : K J) (k : K) :
(c.whisker g).ι k = c.ι (g k)

Taking the cone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cone and postcomposing with a suitable isomorphism.

Equations

Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cocone and precomposing with a suitable isomorphism.

Equations

Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.

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

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

Instances for category_theory.limits.limit_bicone
  • category_theory.limits.limit_bicone.has_sizeof_inst
@[class]
structure category_theory.limits.has_biproduct {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (F : J → C) :
Prop

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

Instances of this typeclass
@[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 of this typeclass
@[reducible]

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

@[reducible]

The projection onto a summand of a biproduct.

@[reducible]

The inclusion into a summand of a biproduct.

Note that as this lemma has a if in the statement, we include a decidable_eq argument. This means you may not be able to simp using this lemma unless you open_locale classical.

@[reducible]
noncomputable def category_theory.limits.biproduct.lift {J : Type w} {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} (p : Π (b : J), P f b) :
P f

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

@[reducible]
noncomputable def category_theory.limits.biproduct.desc {J : Type w} {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} (p : Π (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]
@[simp]
@[reducible]

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.

@[reducible]

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

@[simp]
theorem category_theory.limits.biproduct.lift_map_assoc {J : Type w} {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {f g : J → C} [category_theory.limits.has_biproduct f] [category_theory.limits.has_biproduct g] {P : C} (k : Π (j : J), P f j) (p : Π (j : J), f j g j) {X' : C} (f' : ( λ (j : J), g j) X') :

Given a collection of isomorphisms between corresponding summands of a pair of biproducts indexed by the same type, we obtain an isomorphism between the biproducts.

Equations

The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.

Equations

The canonical morphism from a biproduct to the biproduct over a restriction of its index type.

Equations
noncomputable def category_theory.limits.biproduct.matrix {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) :
f g

Convert a (dependently typed) matrix to a morphism of biproducts.

Equations
@[simp]
theorem category_theory.limits.biproduct.matrix_π_assoc {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) (k : K) {X' : C} (f' : g k X') :
@[simp]
theorem category_theory.limits.biproduct.ι_matrix_assoc {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) (j : J) {X' : C} (f' : ( λ (k : K), g k) X') :
noncomputable def category_theory.limits.biproduct.components {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : f g) (j : J) (k : K) :
f j g k

Extract the matrix components from a morphism of biproducts.

Equations
@[simp]
noncomputable def category_theory.limits.biproduct.matrix_equiv {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} :
( f g) Π (j : J) (k : K), f j g k

Morphisms between direct sums are matrices.

Equations
@[simp]

Biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biproduct.lift b.π and biproduct.desc b.ι are inverses of each other.

Equations

A biproduct over a index type with exactly one term is just the object over that term.

Equations
@[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

Instances for category_theory.limits.binary_bicone
  • category_theory.limits.binary_bicone.has_sizeof_inst
@[nolint]

Structure witnessing that a binary bicone is a limit cone and a limit cocone.

Instances for category_theory.limits.binary_bicone.is_bilimit
  • category_theory.limits.binary_bicone.is_bilimit.has_sizeof_inst
@[nolint]

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

Instances for category_theory.limits.binary_biproduct_data
  • category_theory.limits.binary_biproduct_data.has_sizeof_inst
@[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 of this typeclass
@[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.

Instances of this typeclass

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.

@[reducible]

An arbitrary choice of biproduct of a pair of objects.

@[reducible]

The projection onto the first summand of a binary biproduct.

@[reducible]

The projection onto the second summand of a binary biproduct.

@[reducible]

The inclusion into the first summand of a binary biproduct.

@[reducible]

The inclusion into the second summand of a binary biproduct.

@[reducible]

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

@[reducible]

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

@[reducible]

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

@[reducible]

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

Binary biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biprod.lift b.fst b.snd and biprod.desc b.inl b.inr are inverses of each other.

Equations

A kernel fork for the kernel of binary_bicone.fst. It consists of the morphism binary_bicone.inr.

Equations

A kernel fork for the kernel of binary_bicone.snd. It consists of the morphism binary_bicone.inl.

Equations

A cokernel cofork for the cokernel of binary_bicone.inl. It consists of the morphism binary_bicone.snd.

Equations

A cokernel cofork for the cokernel of binary_bicone.inr. It consists of the morphism binary_bicone.fst.

Equations
def category_theory.limits.is_bilimit_of_total {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {f : J → C} (b : category_theory.limits.bicone f) (total : finset.univ.sum (λ (j : J), b.π j b.ι j) = 𝟙 b.X) :

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

Equations
theorem category_theory.limits.is_bilimit.total {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {f : J → C} {b : category_theory.limits.bicone f} (i : b.is_bilimit) :
finset.univ.sum (λ (j : J), b.π j b.ι j) = 𝟙 b.X

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, any finite bicone which is a limit cone is in fact a bilimit bicone.

Equations

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

In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

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} [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} [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') :
@[simp]
theorem category_theory.limits.biproduct.matrix_desc_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) {P : C} (x : Π (k : K), g k P) {X' : C} (f' : P X') :
@[simp]
theorem category_theory.limits.biproduct.matrix_desc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) {P : C} (x : Π (k : K), g k P) :
@[simp]
theorem category_theory.limits.biproduct.lift_matrix {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} {P : C} (x : Π (j : J), P f j) (m : Π (j : J) (k : K), f j g k) :
@[simp]
theorem category_theory.limits.biproduct.lift_matrix_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g : K → C} {P : C} (x : Π (j : J), P f j) (m : Π (j : J) (k : K), f j g k) {X' : C} (f' : ( λ (k : K), g k) X') :
theorem category_theory.limits.biproduct.matrix_map_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g h : K → C} (m : Π (j : J) (k : K), f j g k) (n : Π (k : K), g k h k) {X' : C} (f' : ( λ (k : K), h k) X') :
theorem category_theory.limits.biproduct.matrix_map {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J → C} {g h : K → C} (m : Π (j : J) (k : K), f j g k) (n : Π (k : K), g k h k) :
theorem category_theory.limits.biproduct.map_matrix {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f g : J → C} {h : K → C} (m : Π (k : J), f k g k) (n : Π (j : J) (k : K), g j h k) :
theorem category_theory.limits.biproduct.map_matrix_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f g : J → C} {h : K → C} (m : Π (k : J), f k g k) (n : Π (j : J) (k : K), g j h k) {X' : C} (f' : ( λ (k : K), h k) X') :

Reindex a categorical biproduct via an equivalence of the index types.

Equations

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

Equations

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') :

Every split mono f with a cokernel induces a binary bicone with f as its inl and the cokernel map as its snd. We will show in is_bilimit_binary_bicone_of_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

Equations

If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit bicone.

Equations

If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit bicone.

Equations

Every split epi f with a kernel induces a binary bicone with f as its snd and the kernel map as its inl. We will show in binary_bicone_of_is_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

Equations

The existence of binary biproducts implies that there is at most one preadditive structure.

The existence of binary biproducts implies that there is at most one preadditive structure.

@[protected, instance]

The existence of binary biproducts implies that there is at most one preadditive structure.

An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.

Equations