# mathlibdocumentation

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.

• any `binary_biproduct` satisfies `total : fst ≫ inl + snd ≫ inr = 𝟙 X`
• any `binary_product` is a `binary_biproduct`
• any `binary_coproduct` is a `binary_biproduct`

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.

• any `biproduct` satisfies `total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`
• any `product` is a `biproduct`
• any `coproduct` is a `biproduct`

## 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} (F : J → C) :
Type (max u v w)
• X : C
• π : Π (j : J), self.X F j
• ι : Π (j : J), F j self.X
• ι_π : (∀ (j j' : J), self.ι j self.π j' = dite (j = j') (λ (h : j = j'), (λ (h : ¬j = j'), 0)) . "obviously"

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} {F : J → C} (j : J) :
B.ι j B.π j = 𝟙 (F j)
@[simp]
theorem category_theory.limits.bicone_ι_π_self_assoc {J : Type w} {C : Type u} {F : J → C} (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} {F : J → C} {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} {F : J → C} {j j' : J} (h : j j') {X' : C} (f' : F j' X') :
B.ι j B.π j' f' = 0 f'
def category_theory.limits.bicone.to_cone {J : Type w} {C : Type u} {F : J → C}  :

Extract the cone from a bicone.

Equations
@[simp]
theorem category_theory.limits.bicone.to_cone_X {J : Type w} {C : Type u} {F : J → C}  :
B.to_cone.X = B.X
@[simp]
theorem category_theory.limits.bicone.to_cone_π_app {J : Type w} {C : Type u} {F : J → C} (j : category_theory.discrete J) :
B.to_cone.π.app j = B.π j.as
theorem category_theory.limits.bicone.to_cone_π_app_mk {J : Type w} {C : Type u} {F : J → C} (j : J) :
B.to_cone.π.app {as := j} = B.π j
def category_theory.limits.bicone.to_cocone {J : Type w} {C : Type u} {F : J → C}  :

Extract the cocone from a bicone.

Equations
@[simp]
theorem category_theory.limits.bicone.to_cocone_X {J : Type w} {C : Type u} {F : J → C}  :
@[simp]
theorem category_theory.limits.bicone.to_cocone_ι_app {J : Type w} {C : Type u} {F : J → C} (j : category_theory.discrete J) :
B.to_cocone.ι.app j = B.ι j.as
theorem category_theory.limits.bicone.to_cocone_ι_app_mk {J : Type w} {C : Type u} {F : J → C} (j : J) :
B.to_cocone.ι.app {as := j} = B.ι j
@[simp]
theorem category_theory.limits.bicone.of_limit_cone_ι {J : Type w} {C : Type u} {f : J → C} (j : J) :
= ht.lift (λ (j' : J), dite (j = j') (λ (h : j = j'), (λ (h : ¬j = j'), 0)))
noncomputable def category_theory.limits.bicone.of_limit_cone {J : Type w} {C : Type u} {f : J → C}  :

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

Equations
@[simp]
theorem category_theory.limits.bicone.of_limit_cone_π {J : Type w} {C : Type u} {f : J → C} (j : J) :
= t.π.app {as := j}
@[simp]
theorem category_theory.limits.bicone.of_limit_cone_X {J : Type w} {C : Type u} {f : J → C}  :
theorem category_theory.limits.bicone.ι_of_is_limit {J : Type w} {C : Type u} {f : J → C} (j : J) :
t.ι j = ht.lift (λ (j' : J), dite (j = j') (λ (h : j = j'), (λ (h : ¬j = j'), 0)))
@[simp]
theorem category_theory.limits.bicone.of_colimit_cocone_π {J : Type w} {C : Type u} {f : J → C} (j : J) :
= ht.desc (λ (j' : J), dite (j' = j) (λ (h : j' = j), (λ (h : ¬j' = j), 0)))
@[simp]
theorem category_theory.limits.bicone.of_colimit_cocone_X {J : Type w} {C : Type u} {f : J → C}  :
@[simp]
theorem category_theory.limits.bicone.of_colimit_cocone_ι {J : Type w} {C : Type u} {f : J → C} (j : J) :
= t.ι.app {as := j}
noncomputable def category_theory.limits.bicone.of_colimit_cocone {J : Type w} {C : Type u} {f : J → C}  :

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} {f : J → C} (j : J) :
t.π j = ht.desc (λ (j' : J), dite (j' = j) (λ (h : j' = j), (λ (h : ¬j' = j), 0)))
@[nolint]
structure category_theory.limits.bicone.is_bilimit {J : Type w} {C : Type u} {F : J → C}  :
Type (max u v w)
• is_limit :
• is_colimit :

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} (x y : B.is_bilimit) (h : x.is_limit = y.is_limit) (h_1 : x.is_colimit = y.is_colimit) :
x = y
theorem category_theory.limits.bicone.is_bilimit.ext_iff {J : Type w} {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {F : J → C} (x y : B.is_bilimit) :
x = y
@[protected, instance]
def category_theory.limits.bicone.subsingleton_is_bilimit {J : Type w} {C : Type u} {f : J → C}  :
@[simp]
theorem category_theory.limits.bicone.whisker_π {J : Type w} {C : Type u} {K : Type w'} {f : J → C} (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} {K : Type w'} {f : J → C} (g : K J) :
(c.whisker g).X = c.X
def category_theory.limits.bicone.whisker {J : Type w} {C : Type u} {K : Type w'} {f : J → C} (g : K J) :

Whisker a bicone with an equivalence between the indexing types.

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

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
def category_theory.limits.bicone.whisker_to_cocone {J : Type w} {C : Type u} {K : Type w'} {f : J → C} (g : K J) :

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
def category_theory.limits.bicone.whisker_is_bilimit_iff {J : Type w} {C : Type u} {K : Type w'} {f : J → C} (g : K J) :

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} (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} (F : J → C) :
Prop
• exists_biproduct :

`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
theorem category_theory.limits.has_biproduct.mk {J : Type w} {C : Type u} {F : J → C}  :
noncomputable def category_theory.limits.get_biproduct_data {J : Type w} {C : Type u} (F : J → C)  :

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

Equations
noncomputable def category_theory.limits.biproduct.bicone {J : Type w} {C : Type u} (F : J → C)  :

A bicone for `F` which is both a limit cone and a colimit cocone.

Equations
noncomputable def category_theory.limits.biproduct.is_bilimit {J : Type w} {C : Type u} (F : J → C)  :

`biproduct.bicone F` is a bilimit bicone.

Equations
noncomputable def category_theory.limits.biproduct.is_limit {J : Type w} {C : Type u} (F : J → C)  :

`biproduct.bicone F` is a limit cone.

Equations
noncomputable def category_theory.limits.biproduct.is_colimit {J : Type w} {C : Type u} (F : J → C)  :

`biproduct.bicone F` is a colimit cocone.

Equations
@[protected, instance]
def category_theory.limits.has_product_of_has_biproduct {J : Type w} {C : Type u} {F : J → C}  :
@[protected, instance]
def category_theory.limits.has_coproduct_of_has_biproduct {J : Type w} {C : Type u} {F : J → C}  :
@[class]
structure category_theory.limits.has_biproducts_of_shape (J : Type w) (C : Type u)  :
Prop
• has_biproduct : ∀ (F : J → C),

`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
@[class]
structure category_theory.limits.has_finite_biproducts (C : Type u)  :
Prop
• has_biproducts_of_shape : ∀ (J : Type) [_inst_3 : fintype J],

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.limits.biproduct_iso {J : Type w} {C : Type u} (F : J → C)  :
F F

The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.

Equations
@[reducible]
noncomputable def category_theory.limits.biproduct {J : Type w} {C : Type u} (f : J → C)  :
C

`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]
noncomputable def category_theory.limits.biproduct.π {J : Type w} {C : Type u} (f : J → C) (b : J) :
f f b

The projection onto a summand of a biproduct.

@[simp]
theorem category_theory.limits.biproduct.bicone_π {J : Type w} {C : Type u} (f : J → C) (b : J) :
@[reducible]
noncomputable def category_theory.limits.biproduct.ι {J : Type w} {C : Type u} (f : J → C) (b : J) :
f b f

The inclusion into a summand of a biproduct.

@[simp]
theorem category_theory.limits.biproduct.bicone_ι {J : Type w} {C : Type u} (f : J → C) (b : J) :
theorem category_theory.limits.biproduct.ι_π {J : Type w} {C : Type u} [decidable_eq J] (f : J → C) (j j' : J) :
= dite (j = j') (λ (h : j = j'), (λ (h : ¬j = j'), 0)

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

theorem category_theory.limits.biproduct.ι_π_assoc {J : Type w} {C : Type u} [decidable_eq J] (f : J → C) (j j' : J) {X' : C} (f' : f j' X') :
= dite (j = j') (λ (h : j = j'), (λ (h : ¬j = j'), 0) f'
@[simp]
theorem category_theory.limits.biproduct.ι_π_self_assoc {J : Type w} {C : Type u} (f : J → C) (j : J) {X' : C} (f' : f j X') :
@[simp]
theorem category_theory.limits.biproduct.ι_π_self {J : Type w} {C : Type u} (f : J → C) (j : J) :
@[simp]
theorem category_theory.limits.biproduct.ι_π_ne {J : Type w} {C : Type u} (f : J → C) {j j' : J} (h : j j') :
@[simp]
theorem category_theory.limits.biproduct.ι_π_ne_assoc {J : Type w} {C : Type u} (f : J → C) {j j' : J} (h : j j') {X' : C} (f' : f j' X') :
= 0 f'
@[reducible]
noncomputable def category_theory.limits.biproduct.lift {J : Type w} {C : Type u} {f : J → C} {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} {f : J → C} {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]
theorem category_theory.limits.biproduct.lift_π_assoc {J : Type w} {C : Type u} {f : J → C} {P : C} (p : Π (b : J), P f b) (j : J) {X' : C} (f' : f j X') :
= p j f'
@[simp]
theorem category_theory.limits.biproduct.lift_π {J : Type w} {C : Type u} {f : J → C} {P : C} (p : Π (b : J), P f b) (j : J) :
@[simp]
theorem category_theory.limits.biproduct.ι_desc {J : Type w} {C : Type u} {f : J → C} {P : C} (p : Π (b : J), f b P) (j : J) :
@[simp]
theorem category_theory.limits.biproduct.ι_desc_assoc {J : Type w} {C : Type u} {f : J → C} {P : C} (p : Π (b : J), f b P) (j : J) {X' : C} (f' : P X') :
= p j f'
@[reducible]
noncomputable def category_theory.limits.biproduct.map {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
f g

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]
noncomputable def category_theory.limits.biproduct.map' {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
f g

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

@[ext]
theorem category_theory.limits.biproduct.hom_ext {J : Type w} {C : Type u} {f : J → C} {Z : C} (g h : Z f) (w : ∀ (j : J), ) :
g = h
@[ext]
theorem category_theory.limits.biproduct.hom_ext' {J : Type w} {C : Type u} {f : J → C} {Z : C} (g h : f Z) (w : ∀ (j : J), ) :
g = h
noncomputable def category_theory.limits.biproduct.iso_product {J : Type w} {C : Type u} (f : J → C)  :
f f

The canonical isomorphism between the chosen biproduct and the chosen product.

Equations
@[simp]
theorem category_theory.limits.biproduct.iso_product_hom {J : Type w} {C : Type u} {f : J → C}  :
@[simp]
theorem category_theory.limits.biproduct.iso_product_inv {J : Type w} {C : Type u} {f : J → C}  :
noncomputable def category_theory.limits.biproduct.iso_coproduct {J : Type w} {C : Type u} (f : J → C)  :
f f

The canonical isomorphism between the chosen biproduct and the chosen coproduct.

Equations
@[simp]
theorem category_theory.limits.biproduct.iso_coproduct_inv {J : Type w} {C : Type u} {f : J → C}  :
@[simp]
theorem category_theory.limits.biproduct.iso_coproduct_hom {J : Type w} {C : Type u} {f : J → C}  :
theorem category_theory.limits.biproduct.map_eq_map' {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
@[simp]
theorem category_theory.limits.biproduct.map_π {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) (j : J) :
@[simp]
theorem category_theory.limits.biproduct.map_π_assoc {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) (j : J) {X' : C} (f' : g j X') :
@[simp]
theorem category_theory.limits.biproduct.ι_map_assoc {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) (j : J) {X' : C} (f' : ( λ (j : J), g j) X') :
@[simp]
theorem category_theory.limits.biproduct.ι_map {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) (j : J) :
@[simp]
theorem category_theory.limits.biproduct.map_desc_assoc {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) {P : C} (k : Π (j : J), g j P) {X' : C} (f' : P X') :
@[simp]
theorem category_theory.limits.biproduct.map_desc {J : Type w} {C : Type u} {f g : J → C} (p : Π (j : J), f j g j) {P : C} (k : Π (j : J), g j P) :
@[simp]
theorem category_theory.limits.biproduct.lift_map_assoc {J : Type w} {C : Type u} {f g : J → C} {P : C} (k : Π (j : J), P f j) (p : Π (j : J), f j g j) {X' : C} (f' : ( λ (j : J), g j) X') :
@[simp]
theorem category_theory.limits.biproduct.lift_map {J : Type w} {C : Type u} {f g : J → C} {P : C} (k : Π (j : J), P f j) (p : Π (j : J), f j g j) :
@[simp]
theorem category_theory.limits.biproduct.map_iso_inv {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
@[simp]
theorem category_theory.limits.biproduct.map_iso_hom {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
noncomputable def category_theory.limits.biproduct.map_iso {J : Type w} {C : Type u} {f g : J → C} (p : Π (b : J), f b g b) :
f g

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
noncomputable def category_theory.limits.biproduct.from_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
f

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

Equations
noncomputable def category_theory.limits.biproduct.to_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
f

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

Equations
@[simp]
theorem category_theory.limits.biproduct.from_subtype_π {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : J) :
= dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0)
@[simp]
theorem category_theory.limits.biproduct.from_subtype_π_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : J) {X' : C} (f' : f j X') :
= dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0) f'
theorem category_theory.limits.biproduct.from_subtype_eq_lift {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
= category_theory.limits.biproduct.lift (λ (j : J), dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0))
@[simp]
theorem category_theory.limits.biproduct.from_subtype_π_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) {X' : C} (f' : f j X') :
@[simp]
theorem category_theory.limits.biproduct.from_subtype_π_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) :
@[simp]
theorem category_theory.limits.biproduct.to_subtype_π_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) {X' : C} (f' : j X') :
@[simp]
theorem category_theory.limits.biproduct.to_subtype_π {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) :
@[simp]
theorem category_theory.limits.biproduct.ι_to_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : J) {X' : C} (f' : X') :
= dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0) f'
@[simp]
theorem category_theory.limits.biproduct.ι_to_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : J) :
= dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0)
theorem category_theory.limits.biproduct.to_subtype_eq_desc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
= category_theory.limits.biproduct.desc (λ (j : J), dite (p j) (λ (h : p j), j, h⟩) (λ (h : ¬p j), 0))
@[simp]
theorem category_theory.limits.biproduct.ι_to_subtype_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) :
@[simp]
theorem category_theory.limits.biproduct.ι_to_subtype_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.biproduct.ι_from_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) :
@[simp]
theorem category_theory.limits.biproduct.ι_from_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) (j : subtype p) {X' : C} (f' : f X') :
@[simp]
theorem category_theory.limits.biproduct.from_subtype_to_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
@[simp]
theorem category_theory.limits.biproduct.from_subtype_to_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.biproduct.to_subtype_from_subtype_assoc {J : Type w} {C : Type u} (f : J → C) (p : J → Prop) {X' : C} (f' : f X') :
= category_theory.limits.biproduct.map (λ (j : J), ite (p j) (𝟙 (f j)) 0) f'
@[simp]
theorem category_theory.limits.biproduct.to_subtype_from_subtype {J : Type w} {C : Type u} (f : J → C) (p : J → Prop)  :
= category_theory.limits.biproduct.map (λ (j : J), ite (p j) (𝟙 (f j)) 0)
noncomputable def category_theory.limits.biproduct.is_limit_from_subtype {J : Type w} {C : Type u} (f : J → C) (i : J) [category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), i j) f)] :

The kernel of `biproduct.π f i` is the inclusion from the biproduct which omits `i` from the index set `J` into the biproduct over `J`.

Equations
noncomputable def category_theory.limits.biproduct.is_colimit_to_subtype {J : Type w} {C : Type u} (f : J → C) (i : J) [category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), i j) f)] :

The cokernel of `biproduct.ι f i` is the projection from the biproduct over the index set `J` onto the biproduct omitting `i`.

Equations
noncomputable def category_theory.limits.biproduct.matrix {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {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_π {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) (k : K) :
@[simp]
theorem category_theory.limits.biproduct.matrix_π_assoc {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {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} {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') :
@[simp]
theorem category_theory.limits.biproduct.ι_matrix {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) (j : J) :
noncomputable def category_theory.limits.biproduct.components {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {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]
theorem category_theory.limits.biproduct.matrix_components {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : Π (j : J) (k : K), f j g k) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.biproduct.components_matrix {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : f g) :
noncomputable def category_theory.limits.biproduct.matrix_equiv {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} :
( f g) Π (j : J) (k : K), f j g k

Morphisms between direct sums are matrices.

Equations
@[simp]
theorem category_theory.limits.biproduct.matrix_equiv_symm_apply {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : Π (j : J) (k : K), (λ (j : J), f j) j (λ (k : K), g k) k) :
@[simp]
theorem category_theory.limits.biproduct.matrix_equiv_apply {J : Type} [fintype J] {K : Type} [fintype K] {C : Type u} {f : J → C} {g : K → C} (m : f g) (j : J) (k : K) :
@[protected, instance]
def category_theory.limits.biproduct.ι_mono {J : Type w} {C : Type u} (f : J → C) (b : J) :
@[protected, instance]
def category_theory.limits.biproduct.π_epi {J : Type w} {C : Type u} (f : J → C) (b : J) :
theorem category_theory.limits.biproduct.cone_point_unique_up_to_iso_hom {J : Type w} {C : Type u} (f : J → C) (hb : b.is_bilimit) :

Auxiliary lemma for `biproduct.unique_up_to_iso`.

theorem category_theory.limits.biproduct.cone_point_unique_up_to_iso_inv {J : Type w} {C : Type u} (f : J → C) (hb : b.is_bilimit) :

Auxiliary lemma for `biproduct.unique_up_to_iso`.

noncomputable def category_theory.limits.biproduct.unique_up_to_iso {J : Type w} {C : Type u} (f : J → C) (hb : b.is_bilimit) :
b.X f

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
@[simp]
theorem category_theory.limits.biproduct.unique_up_to_iso_hom {J : Type w} {C : Type u} (f : J → C) (hb : b.is_bilimit) :
@[simp]
theorem category_theory.limits.biproduct.unique_up_to_iso_inv {J : Type w} {C : Type u} (f : J → C) (hb : b.is_bilimit) :
@[protected, instance]

A category with finite biproducts has a zero object.

@[simp]
theorem category_theory.limits.limit_bicone_of_unique_bicone_ι {J : Type w} {C : Type u} [unique J] (f : J → C) (j : J) :
@[simp]
theorem category_theory.limits.limit_bicone_of_unique_is_bilimit_is_colimit {J : Type w} {C : Type u} [unique J] (f : J → C) :
def category_theory.limits.limit_bicone_of_unique {J : Type w} {C : Type u} [unique J] (f : J → C) :

The limit bicone for the biproduct over an index type with exactly one term.

Equations
@[simp]
theorem category_theory.limits.limit_bicone_of_unique_bicone_X {J : Type w} {C : Type u} [unique J] (f : J → C) :
@[simp]
theorem category_theory.limits.limit_bicone_of_unique_bicone_π {J : Type w} {C : Type u} [unique J] (f : J → C) (j : J) :
@[simp]
theorem category_theory.limits.limit_bicone_of_unique_is_bilimit_is_limit {J : Type w} {C : Type u} [unique J] (f : J → C) :
@[protected, instance]
def category_theory.limits.has_biproduct_unique {J : Type w} {C : Type u} [unique J] (f : J → C) :
noncomputable def category_theory.limits.biproduct_unique_iso {J : Type w} {C : Type u} [unique J] (f : J → C) :

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

Equations
@[simp]
theorem category_theory.limits.biproduct_unique_iso_hom {J : Type w} {C : Type u} [unique J] (f : J → C) :
@[simp]
theorem category_theory.limits.biproduct_unique_iso_inv {J : Type w} {C : Type u} [unique J] (f : J → C) :
@[nolint]
structure category_theory.limits.binary_bicone {C : Type u} (P Q : C) :
Type (max u v)

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
@[simp]
theorem category_theory.limits.binary_bicone.inl_fst {C : Type u} {P Q : C} (self : Q) :
self.inl self.fst = 𝟙 P
@[simp]
theorem category_theory.limits.binary_bicone.inl_snd {C : Type u} {P Q : C} (self : Q) :
self.inl self.snd = 0
@[simp]
theorem category_theory.limits.binary_bicone.inr_fst {C : Type u} {P Q : C} (self : Q) :
self.inr self.fst = 0
@[simp]
theorem category_theory.limits.binary_bicone.inr_snd {C : Type u} {P Q : C} (self : Q) :
self.inr self.snd = 𝟙 Q
@[simp]
theorem category_theory.limits.binary_bicone.inr_snd_assoc {C : Type u} {P Q : C} (self : Q) {X' : C} (f' : Q X') :
self.inr self.snd f' = f'
@[simp]
theorem category_theory.limits.binary_bicone.inl_fst_assoc {C : Type u} {P Q : C} (self : Q) {X' : C} (f' : P X') :
self.inl self.fst f' = f'
@[simp]
theorem category_theory.limits.binary_bicone.inr_fst_assoc {C : Type u} {P Q : C} (self : Q) {X' : C} (f' : P X') :
self.inr self.fst f' = 0 f'
@[simp]
theorem category_theory.limits.binary_bicone.inl_snd_assoc {C : Type u} {P Q : C} (self : Q) {X' : C} (f' : Q X') :
self.inl self.snd f' = 0 f'
def category_theory.limits.binary_bicone.to_cone {C : Type u} {P Q : C}  :

Extract the cone from a binary bicone.

Equations
@[simp]
theorem category_theory.limits.binary_bicone.to_cone_X {C : Type u} {P Q : C}  :
c.to_cone.X = c.X
@[simp]
@[simp]
@[simp]
@[simp]

Extract the cocone from a binary bicone.

Equations
@[simp]
theorem category_theory.limits.binary_bicone.to_cocone_X {C : Type u} {P Q : C}  :
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem category_theory.limits.binary_bicone.to_bicone_ι {C : Type u} {X Y : C}  :
b.to_bicone.ι j = j.cases_on b.inl b.inr

Convert a `binary_bicone` into a `bicone` over a pair.

Equations
@[simp]
theorem category_theory.limits.binary_bicone.to_bicone_π {C : Type u} {X Y : C}  :
b.to_bicone.π j = j.cases_on b.fst b.snd
@[simp]
theorem category_theory.limits.binary_bicone.to_bicone_X {C : Type u} {X Y : C}  :

A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.

Equations

A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit cocone.

Equations
@[simp]

Convert a `bicone` over a function on `walking_pair` to a binary_bicone.

Equations
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_X {C : Type u} {X Y : C}  :
@[simp]
@[simp]
@[simp]

A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit cone.

Equations

A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a colimit cocone.

Equations
@[nolint]
structure category_theory.limits.binary_bicone.is_bilimit {C : Type u} {P Q : C}  :
Type (max u v)
• is_limit :
• is_colimit :

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

A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.

Equations

A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a bilimit.

Equations
@[nolint]
structure category_theory.limits.binary_biproduct_data {C : Type u} (P Q : C) :
Type (max u v)

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]
structure category_theory.limits.has_binary_biproduct {C : Type u} (P Q : C) :
Prop
• exists_binary_biproduct :

`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
theorem category_theory.limits.has_binary_biproduct.mk {C : Type u} {P Q : C}  :
noncomputable def category_theory.limits.get_binary_biproduct_data {C : Type u} (P Q : C)  :

Use the axiom of choice to extract explicit `binary_biproduct_data F` from `has_binary_biproduct F`.

Equations
noncomputable def category_theory.limits.binary_biproduct.bicone {C : Type u} (P Q : C)  :

A bicone for `P Q` which is both a limit cone and a colimit cocone.

Equations
noncomputable def category_theory.limits.binary_biproduct.is_bilimit {C : Type u} (P Q : C)  :

`binary_biproduct.bicone P Q` is a limit bicone.

Equations
noncomputable def category_theory.limits.binary_biproduct.is_limit {C : Type u} (P Q : C)  :

`binary_biproduct.bicone P Q` is a limit cone.

Equations

`binary_biproduct.bicone P Q` is a colimit cocone.

Equations
@[class]
structure category_theory.limits.has_binary_biproducts (C : Type u)  :
Prop
• has_binary_biproduct : ∀ (P Q : C),

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.limits.biprod_iso {C : Type u} (X Y : C)  :
X Y X ⨿ Y

The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.

Equations
@[reducible]
noncomputable def category_theory.limits.biprod {C : Type u} (X Y : C)  :
C

An arbitrary choice of biproduct of a pair of objects.

@[reducible]
noncomputable def category_theory.limits.biprod.fst {C : Type u} {X Y : C}  :
X Y X

The projection onto the first summand of a binary biproduct.

@[reducible]
noncomputable def category_theory.limits.biprod.snd {C : Type u} {X Y : C}  :
X Y Y

The projection onto the second summand of a binary biproduct.

@[reducible]
noncomputable def category_theory.limits.biprod.inl {C : Type u} {X Y : C}  :
X X Y

The inclusion into the first summand of a binary biproduct.

@[reducible]
noncomputable def category_theory.limits.biprod.inr {C : Type u} {X Y : C}  :
Y X Y

The inclusion into the second summand of a binary biproduct.

@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.biprod.inl_fst_assoc {C : Type u} {X Y : C} {X' : C} (f' : X X') :
@[simp]
@[simp]
theorem category_theory.limits.biprod.inl_snd_assoc {C : Type u} {X Y : C} {X' : C} (f' : Y X') :
@[simp]
@[simp]
theorem category_theory.limits.biprod.inr_fst_assoc {C : Type u} {X Y : C} {X' : C} (f' : X X') :
@[simp]
@[simp]
theorem category_theory.limits.biprod.inr_snd_assoc {C : Type u} {X Y : C} {X' : C} (f' : Y X') :
@[reducible]
noncomputable def category_theory.limits.biprod.lift {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
W X Y

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

@[reducible]
noncomputable def category_theory.limits.biprod.desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
X Y W

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

@[simp]
theorem category_theory.limits.biprod.lift_fst_assoc {C : Type u} {W X Y : C} (f : W X) (g : W Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.biprod.lift_fst {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
@[simp]
theorem category_theory.limits.biprod.lift_snd {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
@[simp]
theorem category_theory.limits.biprod.lift_snd_assoc {C : Type u} {W X Y : C} (f : W X) (g : W Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.biprod.inl_desc_assoc {C : Type u} {W X Y : C} (f : X W) (g : Y W) {X' : C} (f' : W X') :
@[simp]
theorem category_theory.limits.biprod.inl_desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
@[simp]
theorem category_theory.limits.biprod.inr_desc_assoc {C : Type u} {W X Y : C} (f : X W) (g : Y W) {X' : C} (f' : W X') :
@[simp]
theorem category_theory.limits.biprod.inr_desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
@[protected, instance]
def category_theory.limits.biprod.mono_lift_of_mono_left {C : Type u} {W X Y : C} (f : W X) (g : W Y)  :
@[protected, instance]
def category_theory.limits.biprod.mono_lift_of_mono_right {C : Type u} {W X Y : C} (f : W X) (g : W Y)  :
@[protected, instance]
def category_theory.limits.biprod.epi_desc_of_epi_left {C : Type u} {W X Y : C} (f : X W) (g : Y W)  :
@[protected, instance]
def category_theory.limits.biprod.epi_desc_of_epi_right {C : Type u} {W X Y : C} (f : X W) (g : Y W)  :
@[reducible]
noncomputable def category_theory.limits.biprod.map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W X Y Z

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

@[reducible]
noncomputable def category_theory.limits.biprod.map' {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W X Y Z

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

@[ext]
theorem category_theory.limits.biprod.hom_ext {C : Type u} {X Y Z : C} (f g : Z X Y)  :
f = g
@[ext]
theorem category_theory.limits.biprod.hom_ext' {C : Type u} {X Y Z : C} (f g : X Y Z)  :
f = g
noncomputable def category_theory.limits.biprod.iso_prod {C : Type u} (X Y : C)  :
X Y X Y

The canonical isomorphism between the chosen biproduct and the chosen product.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.biprod.iso_coprod {C : Type u} (X Y : C)  :
X Y X ⨿ Y

The canonical isomorphism between the chosen biproduct and the chosen coproduct.

Equations
@[simp]
@[simp]
theorem category_theory.limits.biprod.map_eq_map' {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem category_theory.limits.biprod.map_fst_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.biprod.map_fst {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.biprod.map_snd {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.biprod.map_snd_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Z X') :
@[simp]
theorem category_theory.limits.biprod.inl_map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.biprod.inl_map_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y Z X') :
@[simp]
theorem category_theory.limits.biprod.inr_map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.biprod.inr_map_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y Z X') :
noncomputable def category_theory.limits.biprod.map_iso {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W X Y Z

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

Equations
@[simp]
theorem category_theory.limits.biprod.map_iso_hom {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.biprod.map_iso_inv {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :

Auxiliary lemma for `biprod.unique_up_to_iso`.