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,
- any
binary_biproductsatisfiestotal : fst ≫ inl + snd ≫ inr = 𝟙 X - any
binary_productis abinary_biproduct - any
binary_coproductis abinary_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.
In a preadditive category,
- any
biproductsatisfiestotal : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f) - any
productis abiproduct - any
coproductis abiproduct
Notation
As ⊕ is already taken for the sum of types, we introduce the notation X ⊞ Y for
a binary biproduct. We introduce ⨁ f for the indexed biproduct.
@[nolint]
structure
category_theory.limits.bicone
{J : Type v}
[decidable_eq J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
(J → C) → Type (max u v)
- X : C
- π : Π (j : J), c.X ⟶ F j
- ι : Π (j : J), F j ⟶ c.X
- ι_π : ∀ (j j' : J), c.ι j ≫ c.π j' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)
A c : bicone F is:
- an object
c.Xand - morphisms
π j : X ⟶ F jandι j : F j ⟶ Xfor eachj, - such that
ι j ≫ π j'is the identity whenj = j'and zero otherwise.
@[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) :
@[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} :
@[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) :
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} :
Extract the cone from a bicone.
@[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) :
@[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) :
@[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) :
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} :
Extract the cocone from a bicone.
@[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] :
(J → C) → Type (max u v)
- bicone : category_theory.limits.bicone F
- is_limit : category_theory.limits.is_limit category_theory.limits.has_biproduct.bicone.to_cone
- is_colimit : category_theory.limits.is_colimit category_theory.limits.has_biproduct.bicone.to_cocone
has_biproduct F represents a particular chosen bicone which is
simultaneously a limit and a colimit of the diagram F.
@[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] :
@[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] :
@[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] :
Type (max u v)
- has_biproduct : Π (F : J → C), category_theory.limits.has_biproduct F
C has biproducts of shape J if we have chosen
a particular limit and a particular colimit, with the same cone points,
of every function F : J → C.
@[class]
structure
category_theory.limits.has_finite_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Type (max u (v+1))
- has_biproducts_of_shape : Π (J : Type ?) [_inst_4 : decidable_eq J] [_inst_5 : fintype J], category_theory.limits.has_biproducts_of_shape J C
has_finite_biproducts C represents a choice of biproduct for every family of objects in C
indexed by a finite type with decidable equality.
@[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] :
Equations
- category_theory.limits.has_finite_products_of_has_finite_biproducts C = λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), {has_limit := λ (F : category_theory.discrete J ⥤ C), category_theory.limits.has_limit_of_iso category_theory.discrete.nat_iso_functor.symm}
@[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] :
Equations
- category_theory.limits.has_finite_coproducts_of_has_finite_biproducts C = λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), {has_colimit := λ (F : category_theory.discrete J ⥤ C), category_theory.limits.has_colimit_of_iso category_theory.discrete.nat_iso_functor}
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] :
The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.
Equations
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.)
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] :
The chosen bicone over a family of elements.
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] :
The cone coming from the chosen bicone is a limit cone.
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] :
The cocone coming from the chosen bicone is a colimit cocone.
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) :
The projection onto a summand of a biproduct.
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) :
The inclusion into a summand of a biproduct.
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'
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)
@[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)
@[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'
@[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'
@[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} :
j ≠ j' → category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' = 0
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} :
Given a collection of maps into the summands, we obtain a map into the biproduct.
def
category_theory.limits.biproduct.desc
{J : Type v}
[decidable_eq J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C} :
Given a collection of maps out of the summands, we obtain a map out of the biproduct.
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] :
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.
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] :
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 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) :
(∀ (j : J), g ≫ category_theory.limits.biproduct.π f j = h ≫ category_theory.limits.biproduct.π f j) → g = h
@[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) :
(∀ (j : J), category_theory.limits.biproduct.ι f j ≫ g = category_theory.limits.biproduct.ι f j ≫ h) → g = h
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) :
@[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) :
Equations
- category_theory.limits.biproduct.ι_mono f b = {retraction := category_theory.limits.biproduct.desc (λ (b' : J), dite (b' = b) (λ (h : b' = b), category_theory.eq_to_hom _) (λ (h : ¬b' = b), category_theory.limits.biproduct.ι f b' ≫ category_theory.limits.biproduct.π f b)), id' := _}
@[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) :
Equations
- category_theory.limits.biproduct.π_epi f b = {section_ := category_theory.limits.biproduct.lift (λ (b' : J), dite (b = b') (λ (h : b = b'), category_theory.eq_to_hom _) (λ (h : ¬b = b'), category_theory.limits.biproduct.ι f b ≫ category_theory.limits.biproduct.π f b')), id' := _}
@[simp]
theorem
category_theory.limits.biproduct.inl_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) :
@[nolint]
structure
category_theory.limits.binary_bicone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
C → C → Type (max u v)
- X : C
- fst : c.X ⟶ P
- snd : c.X ⟶ Q
- inl : P ⟶ c.X
- inr : Q ⟶ c.X
- inl_fst' : c.inl ≫ c.fst = 𝟙 P . "obviously"
- inl_snd' : c.inl ≫ c.snd = 0 . "obviously"
- inr_fst' : c.inr ≫ c.fst = 0 . "obviously"
- inr_snd' : c.inr ≫ c.snd = 𝟙 Q . "obviously"
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
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} :
Extract the cone from a binary bicone.
Equations
@[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) :
@[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) :
@[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) :
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} :
Extract the cocone from a binary bicone.
Equations
@[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) :
@[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) :
@[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) :
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} :
Convert a bicone over a function on walking_pair to a binary_bicone.
Equations
- b.to_binary_bicone = {X := b.X, fst := b.π category_theory.limits.walking_pair.left, snd := b.π category_theory.limits.walking_pair.right, inl := b.ι category_theory.limits.walking_pair.left, inr := b.ι category_theory.limits.walking_pair.right, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[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) :
@[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) :
@[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) :
@[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
@[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) :
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} :
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
- category_theory.limits.bicone.to_binary_bicone_is_limit c = {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair X Y)), c.lift s, fac' := _, uniq' := _}
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} :
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
- category_theory.limits.bicone.to_binary_bicone_is_colimit c = {desc := λ (s : category_theory.limits.cocone (category_theory.limits.pair X Y)), c.desc s, fac' := _, uniq' := _}
@[class]
structure
category_theory.limits.has_binary_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
C → C → Type (max u v)
- bicone : category_theory.limits.binary_bicone P Q
- is_limit : category_theory.limits.is_limit category_theory.limits.has_binary_biproduct.bicone.to_cone
- is_colimit : category_theory.limits.is_colimit category_theory.limits.has_binary_biproduct.bicone.to_cocone
has_binary_biproduct P Q represents a particular chosen bicone which is
simultaneously a limit and a colimit of the diagram pair P Q.
@[class]
structure
category_theory.limits.has_binary_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Type (max u v)
- has_binary_biproduct : Π (P Q : C), category_theory.limits.has_binary_biproduct P Q
has_binary_biproducts C represents a particular chosen bicone which is
simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.
def
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] :
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.
Equations
- category_theory.limits.has_binary_biproducts_of_finite_biproducts C = {has_binary_biproduct := λ (P Q : C), {bicone := (category_theory.limits.biproduct.bicone (category_theory.limits.pair P Q).obj).to_binary_bicone, is_limit := category_theory.limits.bicone.to_binary_bicone_is_limit (category_theory.limits.biproduct.is_limit (category_theory.limits.pair P Q).obj), is_colimit := category_theory.limits.bicone.to_binary_bicone_is_colimit (category_theory.limits.biproduct.is_colimit (category_theory.limits.pair P Q).obj)}}
@[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] :
@[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] :
@[instance]
@[instance]
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] :
The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.
Equations
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
The chosen biproduct of a pair of objects.
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] :
The projection onto the first summand of a binary biproduct.
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] :
The projection onto the second summand of a binary biproduct.
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] :
The inclusion into the first summand of a binary biproduct.
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] :
The inclusion into the second summand of a binary biproduct.
@[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] :
@[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') :
@[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') :
@[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] :
@[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] :
@[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') :
@[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] :
@[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') :
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] :
Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.
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] :
Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.
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] :
Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.
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] :
Given a pair of isomorphisms between the summands of a pair of binary biproducts, we obtain an isomorphism between the binary biproducts.
Equations
- category_theory.limits.biprod.map_iso f g = {hom := category_theory.limits.biprod.map f.hom g.hom, inv := category_theory.limits.biprod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
@[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) :
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] :
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}
[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) :
@[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) :
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) :
@[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] :
@[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] :
@[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] :
@[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] :
@[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') :
@[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) :
@[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) :
@[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') :
@[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') :
@[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) :
@[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') :
@[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) :
@[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) :
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) :
The braiding isomorphism which swaps a binary biproduct.
Equations
- category_theory.limits.biprod.braiding P Q = {hom := category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst, inv := category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
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) :
An alternative formula for the braiding isomorphism which swaps a binary biproduct, using the fact that the biproduct is a coproduct.
Equations
- category_theory.limits.biprod.braiding' P Q = {hom := category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl, inv := category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
@[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) :
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} :
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) :
The braiding isomorphism can be passed through a map by swapping the order.
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') :
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') :
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) :
@[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) :
@[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') :
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'
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.
def
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) :
finset.univ.sum (λ (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.)
Equations
- category_theory.limits.has_biproduct_of_total b total = {bicone := b, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor f)), finset.univ.sum (λ (j : category_theory.discrete J), s.π.app j ≫ b.ι j), fac' := _, uniq' := _}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.discrete.functor f)), finset.univ.sum (λ (j : J), b.π j ≫ s.ι.app j), fac' := _, uniq' := _}}
def
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] :
In a preadditive category, if the product over f : J → C exists,
then the biproduct over f exists.
Equations
- category_theory.limits.has_biproduct.of_has_product f = category_theory.limits.has_biproduct_of_total {X := ∏ f, π := category_theory.limits.pi.π f _inst_5, ι := λ (j : J), category_theory.limits.pi.lift (λ (j' : J), dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)), ι_π := _} _
def
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] :
In a preadditive category, if the coproduct over f : J → C exists,
then the biproduct over f exists.
Equations
- category_theory.limits.has_biproduct.of_has_coproduct f = category_theory.limits.has_biproduct_of_total {X := ∐ f, π := λ (j : J), category_theory.limits.sigma.desc (λ (j' : J), dite (j' = j) (λ (h : j' = j), category_theory.eq_to_hom _) (λ (h : ¬j' = j), 0)), ι := category_theory.limits.sigma.ι f _inst_5, ι_π := _} _
def
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] :
A preadditive category with finite products has finite biproducts.
Equations
- category_theory.limits.has_finite_biproducts.of_has_finite_products = {has_biproducts_of_shape := λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), {has_biproduct := λ (F : J → C), category_theory.limits.has_biproduct.of_has_product F}}
def
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] :
A preadditive category with finite coproducts has finite biproducts.
Equations
- category_theory.limits.has_finite_biproducts.of_has_finite_coproducts = {has_biproducts_of_shape := λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), {has_biproduct := λ (F : J → C), category_theory.limits.has_biproduct.of_has_coproduct F}}
@[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] :
finset.univ.sum (λ (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)
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 = finset.univ.sum (λ (j : J), g j ≫ category_theory.limits.biproduct.ι f j)
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 = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π f j ≫ g j)
@[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' = finset.univ.sum (λ (j : J), g j ≫ h j) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.lift_desc
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{J : Type v}
[decidable_eq J]
[fintype J]
{f : J → C}
[category_theory.limits.has_biproduct f]
{T U : C}
{g : Π (j : J), T ⟶ f j}
{h : Π (j : J), f j ⟶ U} :
category_theory.limits.biproduct.lift g ≫ category_theory.limits.biproduct.desc h = finset.univ.sum (λ (j : J), g j ≫ h j)
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 = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π f j ≫ h j ≫ category_theory.limits.biproduct.ι g j)
def
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) :
In a preadditive category, we can construct a binary biproduct for X Y : C from
any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.
(That is, such a bicone is a limit cone and a colimit cocone.)
Equations
- category_theory.limits.has_binary_biproduct_of_total b total = {bicone := b, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair X Y)), category_theory.limits.binary_fan.fst s ≫ b.inl + category_theory.limits.binary_fan.snd s ≫ b.inr, fac' := _, uniq' := _}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.limits.pair X Y)), b.fst ≫ category_theory.limits.binary_cofan.inl s + b.snd ≫ category_theory.limits.binary_cofan.inr s, fac' := _, uniq' := _}}
def
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] :
In a preadditive category, if the product of X and Y exists, then the
binary biproduct of X and Y exists.
Equations
- category_theory.limits.has_binary_biproduct.of_has_binary_product X Y = category_theory.limits.has_binary_biproduct_of_total {X := X ⨯ Y, fst := category_theory.limits.prod.fst _inst_5, snd := category_theory.limits.prod.snd _inst_5, inl := category_theory.limits.prod.lift (𝟙 X) 0, inr := category_theory.limits.prod.lift 0 (𝟙 Y), inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _} _
def
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] :
In a preadditive category, if all binary products exist, then all binary biproducts exist.
def
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] :
In a preadditive category, if the coproduct of X and Y exists, then the
binary biproduct of X and Y exists.
Equations
- category_theory.limits.has_binary_biproduct.of_has_binary_coproduct X Y = category_theory.limits.has_binary_biproduct_of_total {X := X ⨿ Y, fst := category_theory.limits.coprod.desc (𝟙 X) 0, snd := category_theory.limits.coprod.desc 0 (𝟙 Y), inl := category_theory.limits.coprod.inl _inst_5, inr := category_theory.limits.coprod.inr _inst_5, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _} _
def
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] :
In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.
@[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] :
In any preadditive category, any binary biproduct satsifies
biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).
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} :
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} :
@[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
@[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'
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} :