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.

source
@[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] (F : 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.
source
@[simp]
theorem category_theory.limits.bicone_ι_π_self {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) :
B.ι j ≫ B.π j = 𝟙 (F j)

source
@[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} (h : j ≠ j') :
B.ι j ≫ B.π j' = 0

source
@[simp]
theorem category_theory.limits.bicone.to_cone_π_app {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 : category_theory.discrete J) :
B.to_cone.π.app j = B.π j

source
@[simp]
theorem category_theory.limits.bicone.to_cone_X {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) :
B.to_cone.X = B.X

source
def category_theory.limits.bicone.to_cone {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) :
category_theory.limits.cone (category_theory.discrete.functor F)

Extract the cone from a bicone.

Equations
source
def category_theory.limits.bicone.to_cocone {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) :
category_theory.limits.cocone (category_theory.discrete.functor F)

Extract the cocone from a bicone.

Equations
source
@[simp]
theorem category_theory.limits.bicone.to_cocone_ι_app {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 : category_theory.discrete J) :
B.to_cocone.ι.app j = B.ι j

source
@[simp]
theorem category_theory.limits.bicone.to_cocone_X {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) :
B.to_cocone.X = B.X

source
@[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] (F : J → C) :
Type (max u v)

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

source
@[class]
structure category_theory.limits.has_biproduct {J : Type v} [decidable_eq J] {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
source
theorem category_theory.limits.has_biproduct.mk {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {F : J → C} (d : category_theory.limits.limit_bicone F) :
category_theory.limits.has_biproduct F

source
def category_theory.limits.get_biproduct_data {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] :
category_theory.limits.limit_bicone F

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

Equations
source
def category_theory.limits.biproduct.bicone {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] :
category_theory.limits.bicone F

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

Equations
source
def category_theory.limits.biproduct.is_limit {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] :
category_theory.limits.is_limit (category_theory.limits.biproduct.bicone F).to_cone

biproduct.bicone F is a limit cone.

Equations
source
def category_theory.limits.biproduct.is_colimit {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] :
category_theory.limits.is_colimit (category_theory.limits.biproduct.bicone F).to_cocone

biproduct.bicone F is a colimit cocone.

Equations
source
@[instance]
def category_theory.limits.has_product_of_has_biproduct {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] :
category_theory.limits.has_limit (category_theory.discrete.functor F)

source
@[instance]
def category_theory.limits.has_coproduct_of_has_biproduct {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] :
category_theory.limits.has_colimit (category_theory.discrete.functor F)

source
@[class]
structure category_theory.limits.has_biproducts_of_shape (J : Type v) [decidable_eq J] (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
Prop

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
source
@[class]
structure category_theory.limits.has_finite_biproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
Prop

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
source
@[instance]
def category_theory.limits.has_finite_products_of_has_finite_biproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] :
category_theory.limits.has_finite_products C

source
@[instance]
def category_theory.limits.has_finite_coproducts_of_has_finite_biproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] :
category_theory.limits.has_finite_coproducts C

source
def category_theory.limits.biproduct_iso {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] :
∏ F ≅ ∐ F

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

Equations
source
def category_theory.limits.biproduct {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] :
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.)

source
def category_theory.limits.biproduct.π {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] (b : J) :
⨁ f ⟶ f b

The projection onto a summand of a biproduct.

source
@[simp]
theorem category_theory.limits.biproduct.bicone_π {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] (b : J) :
(category_theory.limits.biproduct.bicone f).π b = category_theory.limits.biproduct.π f b

source
def category_theory.limits.biproduct.ι {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] (b : J) :
f b ⟶ ⨁ f

The inclusion into a summand of a biproduct.

source
@[simp]
theorem category_theory.limits.biproduct.bicone_ι {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] (b : J) :
(category_theory.limits.biproduct.bicone f).ι b = category_theory.limits.biproduct.ι f b

source
theorem category_theory.limits.biproduct.ι_π {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] (j j' : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)

source
theorem category_theory.limits.biproduct.ι_π_assoc {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] (j j' : J) {X' : C} (f' : f j' ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' ≫ f' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0) ≫ f'

source
@[simp]
theorem category_theory.limits.biproduct.ι_π_self_assoc {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] (j : J) {X' : C} (f' : f j ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j ≫ f' = f'

source
@[simp]
theorem category_theory.limits.biproduct.ι_π_self {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] (j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j = 𝟙 (f j)

source
@[simp]
theorem category_theory.limits.biproduct.ι_π_ne {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] {j j' : J} (h : j ≠ j') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' = 0

source
@[simp]
theorem category_theory.limits.biproduct.ι_π_ne_assoc {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] {j j' : J} (h : j ≠ j') {X' : C} (f' : f j' ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' ≫ f' = 0 ≫ f'

source
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} (p : Π (b : J), P ⟶ f b) :
P ⟶ ⨁ f

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

source
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} (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.

source
@[simp]
theorem category_theory.limits.biproduct.lift_π_assoc {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} (p : Π (b : J), P ⟶ f b) (j : J) {X' : C} (f' : f j ⟶ X') :
category_theory.limits.biproduct.lift p ≫ category_theory.limits.biproduct.π f j ≫ f' = p j ≫ f'

source
@[simp]
theorem 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} (p : Π (b : J), P ⟶ f b) (j : J) :
category_theory.limits.biproduct.lift p ≫ category_theory.limits.biproduct.π f j = p j

source
@[simp]
theorem 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} (p : Π (b : J), f b ⟶ P) (j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.desc p = p j

source
@[simp]
theorem category_theory.limits.biproduct.ι_desc_assoc {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} (p : Π (b : J), f b ⟶ P) (j : J) {X' : C} (f' : P ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.desc p ≫ f' = p j ≫ f'

source
def category_theory.limits.biproduct.map {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts 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.

source
def category_theory.limits.biproduct.map' {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts 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.

source
@[ext]
theorem category_theory.limits.biproduct.hom_ext {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] {Z : C} (g h : Z ⟶ ⨁ f) (w : ∀ (j : J), g ≫ category_theory.limits.biproduct.π f j = h ≫ category_theory.limits.biproduct.π f j) :
g = h

source
@[ext]
theorem category_theory.limits.biproduct.hom_ext' {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] {Z : C} (g h : ⨁ f ⟶ Z) (w : ∀ (j : J), category_theory.limits.biproduct.ι f j ≫ g = category_theory.limits.biproduct.ι f j ≫ h) :
g = h

source
theorem category_theory.limits.biproduct.map_eq_map' {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts C] (p : Π (b : J), f b ⟶ g b) :
category_theory.limits.biproduct.map p = category_theory.limits.biproduct.map' p

source
@[instance]
def category_theory.limits.biproduct.ι_mono {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] (b : J) :
category_theory.split_mono (category_theory.limits.biproduct.ι f b)

Equations
source
@[instance]
def category_theory.limits.biproduct.π_epi {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] (b : J) :
category_theory.split_epi (category_theory.limits.biproduct.π f b)

Equations
source
@[simp]
theorem category_theory.limits.biproduct.map_π {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts C] (p : Π (j : J), f j ⟶ g j) (j : J) :
category_theory.limits.biproduct.map p ≫ category_theory.limits.biproduct.π g j = category_theory.limits.biproduct.π f j ≫ p j

source
@[simp]
theorem category_theory.limits.biproduct.map_π_assoc {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts C] (p : Π (j : J), f j ⟶ g j) (j : J) {X' : C} (f' : g j ⟶ X') :
category_theory.limits.biproduct.map p ≫ category_theory.limits.biproduct.π g j ≫ f' = category_theory.limits.biproduct.π f j ≫ p j ≫ f'

source
@[simp]
theorem category_theory.limits.biproduct.ι_map_assoc {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts C] (p : Π (j : J), f j ⟶ g j) (j : J) {X' : C} (f' : (⨁ λ (j : J), g j) ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.map p ≫ f' = p j ≫ category_theory.limits.biproduct.ι g j ≫ f'

source
@[simp]
theorem category_theory.limits.biproduct.ι_map {J : Type v} [decidable_eq J] {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [fintype J] {f g : J → C} [category_theory.limits.has_finite_biproducts C] (p : Π (j : J), f j ⟶ g j) (j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.map p = p j ≫ category_theory.limits.biproduct.ι g j

source
@[nolint]
structure category_theory.limits.binary_bicone {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (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

source
@[simp]
theorem category_theory.limits.binary_bicone.inl_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.inl ≫ c.fst = 𝟙 P

source
@[simp]
theorem category_theory.limits.binary_bicone.inl_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.inl ≫ c.snd = 0

source
@[simp]
theorem category_theory.limits.binary_bicone.inr_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.inr ≫ c.fst = 0

source
@[simp]
theorem category_theory.limits.binary_bicone.inr_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.inr ≫ c.snd = 𝟙 Q

source
@[simp]
theorem category_theory.limits.binary_bicone.inr_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) {X' : C} (f' : Q ⟶ X') :
c.inr ≫ c.snd ≫ f' = f'

source
@[simp]
theorem category_theory.limits.binary_bicone.inl_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) {X' : C} (f' : P ⟶ X') :
c.inl ≫ c.fst ≫ f' = f'

source
@[simp]
theorem category_theory.limits.binary_bicone.inr_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) {X' : C} (f' : P ⟶ X') :
c.inr ≫ c.fst ≫ f' = 0 ≫ f'

source
@[simp]
theorem category_theory.limits.binary_bicone.inl_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) {X' : C} (f' : Q ⟶ X') :
c.inl ≫ c.snd ≫ f' = 0 ≫ f'

source
def category_theory.limits.binary_bicone.to_cone {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
category_theory.limits.cone (category_theory.limits.pair P Q)

Extract the cone from a binary bicone.

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

source
@[simp]
theorem category_theory.limits.binary_bicone.to_cone_π_app_left {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.to_cone.π.app category_theory.limits.walking_pair.left = c.fst

source
@[simp]
theorem category_theory.limits.binary_bicone.to_cone_π_app_right {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.to_cone.π.app category_theory.limits.walking_pair.right = c.snd

source
def category_theory.limits.binary_bicone.to_cocone {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
category_theory.limits.cocone (category_theory.limits.pair P Q)

Extract the cocone from a binary bicone.

Equations
source
@[simp]
theorem category_theory.limits.binary_bicone.to_cocone_X {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.to_cocone.X = c.X

source
@[simp]
theorem category_theory.limits.binary_bicone.to_cocone_ι_app_left {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.to_cocone.ι.app category_theory.limits.walking_pair.left = c.inl

source
@[simp]
theorem category_theory.limits.binary_bicone.to_cocone_ι_app_right {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (c : category_theory.limits.binary_bicone P Q) :
c.to_cocone.ι.app category_theory.limits.walking_pair.right = c.inr

source
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_inl {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
b.to_binary_bicone.inl = b.ι category_theory.limits.walking_pair.left

source
def category_theory.limits.bicone.to_binary_bicone {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
category_theory.limits.binary_bicone X Y

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

Equations
source
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_X {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
b.to_binary_bicone.X = b.X

source
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
b.to_binary_bicone.fst = b.π category_theory.limits.walking_pair.left

source
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
b.to_binary_bicone.snd = b.π category_theory.limits.walking_pair.right

source
@[simp]
theorem category_theory.limits.bicone.to_binary_bicone_inr {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj) :
b.to_binary_bicone.inr = b.ι category_theory.limits.walking_pair.right

source
def category_theory.limits.bicone.to_binary_bicone_is_limit {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} {b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj} (c : category_theory.limits.is_limit b.to_cone) :
category_theory.limits.is_limit b.to_binary_bicone.to_cone

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
source
def category_theory.limits.bicone.to_binary_bicone_is_colimit {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} {b : category_theory.limits.bicone (category_theory.limits.pair X Y).obj} (c : category_theory.limits.is_colimit b.to_cocone) :
category_theory.limits.is_colimit b.to_binary_bicone.to_cocone

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
source
@[nolint]
structure category_theory.limits.binary_biproduct_data {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) :
Type (max u v)

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

source
@[class]
structure category_theory.limits.has_binary_biproduct {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) :
Prop

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
source
theorem category_theory.limits.has_binary_biproduct.mk {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} (d : category_theory.limits.binary_biproduct_data P Q) :
category_theory.limits.has_binary_biproduct P Q

source
def category_theory.limits.get_binary_biproduct_data {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.binary_biproduct_data P Q

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

Equations
source
def category_theory.limits.binary_biproduct.bicone {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.binary_bicone P Q

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

Equations
source
def category_theory.limits.binary_biproduct.is_limit {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.is_limit (category_theory.limits.binary_biproduct.bicone P Q).to_cone

binary_biproduct.bicone P Q is a limit cone.

Equations
source
def category_theory.limits.binary_biproduct.is_colimit {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (P Q : C) [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.is_colimit (category_theory.limits.binary_biproduct.bicone P Q).to_cocone

binary_biproduct.bicone P Q is a colimit cocone.

Equations
source
@[class]
structure category_theory.limits.has_binary_biproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
Prop

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.

source
theorem category_theory.limits.has_binary_biproducts_of_finite_biproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_finite_biproducts C] :
category_theory.limits.has_binary_biproducts 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.

source
@[instance]
def category_theory.limits.has_binary_biproduct.has_limit_pair {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.has_limit (category_theory.limits.pair P Q)

source
@[instance]
def category_theory.limits.has_binary_biproduct.has_colimit_pair {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {P Q : C} [category_theory.limits.has_binary_biproduct P Q] :
category_theory.limits.has_colimit (category_theory.limits.pair P Q)

source
@[instance]
def category_theory.limits.has_binary_products_of_has_binary_biproducts {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] :
category_theory.limits.has_binary_products C

source
@[instance]
def category_theory.limits.has_binary_coproducts_of_has_binary_biproducts {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] :
category_theory.limits.has_binary_coproducts C

source
def category_theory.limits.biprod_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_biproduct X Y] :
X ⨯ Y ≅ X ⨿ Y

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

Equations
source
def category_theory.limits.biprod {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_biproduct X Y] :
C

An arbitrary choice of biproduct of a pair of objects.

source
def category_theory.limits.biprod.fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
X ⊞ Y ⟶ X

The projection onto the first summand of a binary biproduct.

source
def category_theory.limits.biprod.snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
X ⊞ Y ⟶ Y

The projection onto the second summand of a binary biproduct.

source
def category_theory.limits.biprod.inl {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
X ⟶ X ⊞ Y

The inclusion into the first summand of a binary biproduct.

source
def category_theory.limits.biprod.inr {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
Y ⟶ X ⊞ Y

The inclusion into the second summand of a binary biproduct.

source
@[simp]
theorem category_theory.limits.binary_biproduct.bicone_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
(category_theory.limits.binary_biproduct.bicone X Y).fst = category_theory.limits.biprod.fst

source
@[simp]
theorem category_theory.limits.binary_biproduct.bicone_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
(category_theory.limits.binary_biproduct.bicone X Y).snd = category_theory.limits.biprod.snd

source
@[simp]
theorem category_theory.limits.binary_biproduct.bicone_inl {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
(category_theory.limits.binary_biproduct.bicone X Y).inl = category_theory.limits.biprod.inl

source
@[simp]
theorem category_theory.limits.binary_biproduct.bicone_inr {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
(category_theory.limits.binary_biproduct.bicone X Y).inr = category_theory.limits.biprod.inr

source
@[simp]
theorem category_theory.limits.biprod.inl_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.fst = 𝟙 X

source
@[simp]
theorem category_theory.limits.biprod.inl_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {X' : C} (f' : X ⟶ X') :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.fst ≫ f' = f'

source
@[simp]
theorem category_theory.limits.biprod.inl_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.snd = 0

source
@[simp]
theorem category_theory.limits.biprod.inl_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {X' : C} (f' : Y ⟶ X') :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.snd ≫ f' = 0 ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inr_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.fst = 0

source
@[simp]
theorem category_theory.limits.biprod.inr_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {X' : C} (f' : X ⟶ X') :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.fst ≫ f' = 0 ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inr_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.snd = 𝟙 Y

source
@[simp]
theorem category_theory.limits.biprod.inr_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {X' : C} (f' : Y ⟶ X') :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.snd ≫ f' = f'

source
def category_theory.limits.biprod.lift {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (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.

source
def category_theory.limits.biprod.desc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (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.

source
@[simp]
theorem category_theory.limits.biprod.lift_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {X' : C} (f' : X ⟶ X') :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.fst ≫ f' = f ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.lift_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.fst = f

source
@[simp]
theorem category_theory.limits.biprod.lift_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.snd = g

source
@[simp]
theorem category_theory.limits.biprod.lift_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.snd ≫ f' = g ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inl_desc_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {X' : C} (f' : W ⟶ X') :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.desc f g ≫ f' = f ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inl_desc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.desc f g = f

source
@[simp]
theorem category_theory.limits.biprod.inr_desc_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {X' : C} (f' : W ⟶ X') :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.desc f g ≫ f' = g ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inr_desc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.desc f g = g

source
@[instance]
def category_theory.limits.biprod.mono_lift_of_mono_left {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [category_theory.mono f] :
category_theory.mono (category_theory.limits.biprod.lift f g)

source
@[instance]
def category_theory.limits.biprod.mono_lift_of_mono_right {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [category_theory.mono g] :
category_theory.mono (category_theory.limits.biprod.lift f g)

source
@[instance]
def category_theory.limits.biprod.epi_desc_of_epi_left {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [category_theory.epi f] :
category_theory.epi (category_theory.limits.biprod.desc f g)

source
@[instance]
def category_theory.limits.biprod.epi_desc_of_epi_right {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y : C} [category_theory.limits.has_binary_biproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [category_theory.epi g] :
category_theory.epi (category_theory.limits.biprod.desc f g)

source
def category_theory.limits.biprod.map {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (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.

source
def category_theory.limits.biprod.map' {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (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.

source
@[ext]
theorem category_theory.limits.biprod.hom_ext {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z : C} [category_theory.limits.has_binary_biproduct X Y] (f g : Z ⟶ X ⊞ Y) (h₀ : f ≫ category_theory.limits.biprod.fst = g ≫ category_theory.limits.biprod.fst) (h₁ : f ≫ category_theory.limits.biprod.snd = g ≫ category_theory.limits.biprod.snd) :
f = g

source
@[ext]
theorem category_theory.limits.biprod.hom_ext' {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z : C} [category_theory.limits.has_binary_biproduct X Y] (f g : X ⊞ Y ⟶ Z) (h₀ : category_theory.limits.biprod.inl ≫ f = category_theory.limits.biprod.inl ≫ g) (h₁ : category_theory.limits.biprod.inr ≫ f = category_theory.limits.biprod.inr ≫ g) :
f = g

source
theorem category_theory.limits.biprod.map_eq_map' {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.biprod.map f g = category_theory.limits.biprod.map' f g

source
@[instance]
def category_theory.limits.biprod.inl_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.split_mono category_theory.limits.biprod.inl

Equations
source
@[instance]
def category_theory.limits.biprod.inr_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.split_mono category_theory.limits.biprod.inr

Equations
source
@[instance]
def category_theory.limits.biprod.fst_epi {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.split_epi category_theory.limits.biprod.fst

Equations
source
@[instance]
def category_theory.limits.biprod.snd_epi {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.split_epi category_theory.limits.biprod.snd

Equations
source
@[simp]
theorem category_theory.limits.biprod.map_fst_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.biprod.map f g ≫ category_theory.limits.biprod.fst ≫ f' = category_theory.limits.biprod.fst ≫ f ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.map_fst {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.biprod.map f g ≫ category_theory.limits.biprod.fst = category_theory.limits.biprod.fst ≫ f

source
@[simp]
theorem category_theory.limits.biprod.map_snd {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.biprod.map f g ≫ category_theory.limits.biprod.snd = category_theory.limits.biprod.snd ≫ g

source
@[simp]
theorem category_theory.limits.biprod.map_snd_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Z ⟶ X') :
category_theory.limits.biprod.map f g ≫ category_theory.limits.biprod.snd ≫ f' = category_theory.limits.biprod.snd ≫ g ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inl_map {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.map f g = f ≫ category_theory.limits.biprod.inl

source
@[simp]
theorem category_theory.limits.biprod.inl_map_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⊞ Z ⟶ X') :
category_theory.limits.biprod.inl ≫ category_theory.limits.biprod.map f g ≫ f' = f ≫ category_theory.limits.biprod.inl ≫ f'

source
@[simp]
theorem category_theory.limits.biprod.inr_map {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.map f g = g ≫ category_theory.limits.biprod.inr

source
@[simp]
theorem category_theory.limits.biprod.inr_map_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⊞ Z ⟶ X') :
category_theory.limits.biprod.inr ≫ category_theory.limits.biprod.map f g ≫ f' = g ≫ category_theory.limits.biprod.inr ≫ f'

source
def category_theory.limits.biprod.map_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (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
source
@[simp]
theorem category_theory.limits.biprod.map_iso_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.biprod.map_iso f g).hom = category_theory.limits.biprod.map f.hom g.hom

source
@[simp]
theorem category_theory.limits.biprod.map_iso_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {W X Y Z : C} [category_theory.limits.has_binary_biproduct W X] [category_theory.limits.has_binary_biproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.biprod.map_iso f g).inv = category_theory.limits.biprod.map f.inv g.inv

source
def category_theory.limits.biprod.braiding {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
P ⊞ Q ≅ Q ⊞ P

The braiding isomorphism which swaps a binary biproduct.

Equations
source
@[simp]
theorem category_theory.limits.biprod.braiding_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
(category_theory.limits.biprod.braiding P Q).hom = category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst

source
@[simp]
theorem category_theory.limits.biprod.braiding_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
(category_theory.limits.biprod.braiding P Q).inv = category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst

source
@[simp]
theorem category_theory.limits.biprod.braiding'_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
(category_theory.limits.biprod.braiding' P Q).inv = category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl

source
def category_theory.limits.biprod.braiding' {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
P ⊞ Q ≅ Q ⊞ P

An alternative formula for the braiding isomorphism which swaps a binary biproduct, using the fact that the biproduct is a coproduct.

Equations
source
@[simp]
theorem category_theory.limits.biprod.braiding'_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
(category_theory.limits.biprod.braiding' P Q).hom = category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl

source
theorem category_theory.limits.biprod.braiding'_eq_braiding {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {P Q : C} :
category_theory.limits.biprod.braiding' P Q = category_theory.limits.biprod.braiding P Q

source
theorem category_theory.limits.biprod.braid_natural_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {X' : C} (f' : W ⊞ Y ⟶ X') :
category_theory.limits.biprod.map f g ≫ (category_theory.limits.biprod.braiding Y W).hom ≫ f' = (category_theory.limits.biprod.braiding X Z).hom ≫ category_theory.limits.biprod.map g f ≫ f'

source
theorem category_theory.limits.biprod.braid_natural {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
category_theory.limits.biprod.map f g ≫ (category_theory.limits.biprod.braiding Y W).hom = (category_theory.limits.biprod.braiding X Z).hom ≫ category_theory.limits.biprod.map g f

The braiding isomorphism can be passed through a map by swapping the order.

source
theorem category_theory.limits.biprod.braiding_map_braiding_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Z ⊞ Y ⟶ X') :
(category_theory.limits.biprod.braiding X W).hom ≫ category_theory.limits.biprod.map f g ≫ (category_theory.limits.biprod.braiding Y Z).hom ≫ f' = category_theory.limits.biprod.map g f ≫ f'

source
theorem category_theory.limits.biprod.braiding_map_braiding {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) :
(category_theory.limits.biprod.braiding X W).hom ≫ category_theory.limits.biprod.map f g ≫ (category_theory.limits.biprod.braiding Y Z).hom = category_theory.limits.biprod.map g f

source
@[simp]
theorem category_theory.limits.biprod.symmetry'_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) {X' : C} (f' : P ⊞ Q ⟶ X') :
category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst ≫ category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst ≫ f' = f'

source
@[simp]
theorem category_theory.limits.biprod.symmetry' {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst ≫ category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst = 𝟙 (P ⊞ Q)

source
theorem category_theory.limits.biprod.symmetry_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) {X' : C} (f' : P ⊞ Q ⟶ X') :
(category_theory.limits.biprod.braiding P Q).hom ≫ (category_theory.limits.biprod.braiding Q P).hom ≫ f' = f'

source
theorem category_theory.limits.biprod.symmetry {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (P Q : C) :
(category_theory.limits.biprod.braiding P Q).hom ≫ (category_theory.limits.biprod.braiding Q P).hom = 𝟙 (P ⊞ Q)

The braiding isomorphism is symmetric.

source
theorem category_theory.limits.has_biproduct_of_total {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type v} [decidable_eq J] [fintype J] {f : J → C} (b : category_theory.limits.bicone f) (total : ∑ (j : J), b.π j ≫ b.ι j = 𝟙 b.X) :
category_theory.limits.has_biproduct f

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

source
theorem category_theory.limits.has_biproduct.of_has_product {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_product f] :
category_theory.limits.has_biproduct f

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

source
theorem category_theory.limits.has_biproduct.of_has_coproduct {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_coproduct f] :
category_theory.limits.has_biproduct f

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

source
theorem category_theory.limits.has_finite_biproducts.of_has_finite_products {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_products C] :
category_theory.limits.has_finite_biproducts C

A preadditive category with finite products has finite biproducts.

source
theorem category_theory.limits.has_finite_biproducts.of_has_finite_coproducts {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :
category_theory.limits.has_finite_biproducts C

A preadditive category with finite coproducts has finite biproducts.

source
@[simp]
theorem category_theory.limits.biproduct.total {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] :
∑ (j : J), category_theory.limits.biproduct.π f j ≫ category_theory.limits.biproduct.ι f j = 𝟙 (⨁ f)

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

source
theorem category_theory.limits.biproduct.lift_eq {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 : C} {g : Π (j : J), T ⟶ f j} :
category_theory.limits.biproduct.lift g = ∑ (j : J), g j ≫ category_theory.limits.biproduct.ι f j

source
theorem category_theory.limits.biproduct.desc_eq {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 : C} {g : Π (j : J), f j ⟶ T} :
category_theory.limits.biproduct.desc g = ∑ (j : J), category_theory.limits.biproduct.π f j ≫ g j

source
@[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} :
category_theory.limits.biproduct.lift g ≫ category_theory.limits.biproduct.desc h = ∑ (j : J), g j ≫ h j

source
@[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') :
category_theory.limits.biproduct.lift g ≫ category_theory.limits.biproduct.desc h ≫ f' = (∑ (j : J), g j ≫ h j) ≫ f'

source
theorem category_theory.limits.biproduct.map_eq {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type v} [decidable_eq J] [fintype J] [category_theory.limits.has_finite_biproducts C] {f g : J → C} {h : Π (j : J), f j ⟶ g j} :
category_theory.limits.biproduct.map h = ∑ (j : J), category_theory.limits.biproduct.π f j ≫ h j ≫ category_theory.limits.biproduct.ι g j

source
theorem category_theory.limits.has_binary_biproduct_of_total {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} (b : category_theory.limits.binary_bicone X Y) (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X) :
category_theory.limits.has_binary_biproduct X Y

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

source
theorem category_theory.limits.has_binary_biproduct.of_has_binary_product {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
category_theory.limits.has_binary_biproduct X Y

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

source
theorem category_theory.limits.has_binary_biproducts.of_has_binary_products {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_products C] :
category_theory.limits.has_binary_biproducts C

In a preadditive category, if all binary products exist, then all binary biproducts exist.

source
theorem category_theory.limits.has_binary_biproduct.of_has_binary_coproduct {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.has_binary_biproduct X Y

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

source
theorem category_theory.limits.has_binary_biproducts.of_has_binary_coproducts {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_coproducts C] :
category_theory.limits.has_binary_biproducts C

In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.

source
@[simp]
theorem category_theory.limits.biprod.total {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] :
category_theory.limits.biprod.fst ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.snd ≫ category_theory.limits.biprod.inr = 𝟙 (X ⊞ Y)

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

source
theorem category_theory.limits.biprod.lift_eq {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {T : C} {f : T ⟶ X} {g : T ⟶ Y} :
category_theory.limits.biprod.lift f g = f ≫ category_theory.limits.biprod.inl + g ≫ category_theory.limits.biprod.inr

source
theorem category_theory.limits.biprod.desc_eq {C : Type u} [category_theory.category C] [category_theory.preadditive C] {X Y : C} [category_theory.limits.has_binary_biproduct X Y] {T : C} {f : X ⟶ T} {g : Y ⟶ T} :
category_theory.limits.biprod.desc f g = category_theory.limits.biprod.fst ≫ f + category_theory.limits.biprod.snd ≫ g

source
@[simp]
theorem category_theory.limits.biprod.lift_desc {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} :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc h i = f ≫ h + g ≫ i

source
@[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') :
category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc h i ≫ f' = (f ≫ h + g ≫ i) ≫ f'

source
theorem category_theory.limits.biprod.map_eq {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} :
category_theory.limits.biprod.map f g = category_theory.limits.biprod.fst ≫ f ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.snd ≫ g ≫ category_theory.limits.biprod.inr