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_biproduct
satisfiestotal : fst ≫ inl + snd ≫ inr = 𝟙 X
- any
binary_product
is abinary_biproduct
- any
binary_coproduct
is 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
biproduct
satisfiestotal : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)
- any
product
is abiproduct
- any
coproduct
is 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.
Implementation #
Prior to #14046, has_finite_biproducts
required a decidable_eq
instance on the indexing type.
As this had no pay-off (everything about limits is non-constructive in mathlib), and occasional cost
(constructing decidability instances appropriate for constructions involving the indexing type),
we made everything classical.
- X : C
- π : Π (j : J), self.X ⟶ F j
- ι : Π (j : J), F j ⟶ self.X
- ι_π : (∀ (j j' : J), self.ι j ≫ self.π j' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)) . "obviously"
A c : bicone F
is:
- an object
c.X
and - morphisms
π j : X ⟶ F j
andι j : F j ⟶ X
for eachj
, - such that
ι j ≫ π j'
is the identity whenj = j'
and zero otherwise.
Instances for category_theory.limits.bicone
- category_theory.limits.bicone.has_sizeof_inst
Extract the cone from a bicone.
Extract the cocone from a bicone.
We can turn any limit cone over a discrete collection of objects into a bicone.
We can turn any colimit cocone over a discrete collection of objects into a bicone.
- is_limit : category_theory.limits.is_limit B.to_cone
- is_colimit : category_theory.limits.is_colimit B.to_cocone
Structure witnessing that a bicone is both a limit cone and a colimit cocone.
Instances for category_theory.limits.bicone.is_bilimit
- category_theory.limits.bicone.is_bilimit.has_sizeof_inst
- category_theory.limits.bicone.subsingleton_is_bilimit
Whisker a bicone with an equivalence between the indexing types.
Taking the cone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cone and postcomposing with a suitable isomorphism.
Equations
Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cocone and precomposing with a suitable isomorphism.
Equations
Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.
Equations
- c.whisker_is_bilimit_iff g = equiv_of_subsingleton_of_subsingleton (λ (hc : (c.whisker g).is_bilimit), {is_limit := let this : category_theory.limits.is_limit ((category_theory.limits.cones.postcompose (category_theory.discrete.functor_comp f ⇑g).inv).obj (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)) := hc.is_limit.of_iso_limit (c.whisker_to_cone g), this : category_theory.limits.is_limit (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone) := ⇑(category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g).symm (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)) this in category_theory.limits.is_limit.of_whisker_equivalence (category_theory.discrete.equivalence g) this, is_colimit := let this : category_theory.limits.is_colimit ((category_theory.limits.cocones.precompose (category_theory.discrete.functor_comp f ⇑g).hom).obj (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)) := hc.is_colimit.of_iso_colimit (c.whisker_to_cocone g), this : category_theory.limits.is_colimit (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone) := ⇑(category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g) (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)) this in category_theory.limits.is_colimit.of_whisker_equivalence (category_theory.discrete.equivalence g) this}) (λ (hc : c.is_bilimit), {is_limit := (⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g).symm (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)).symm) (hc.is_limit.whisker_equivalence (category_theory.discrete.equivalence g))).of_iso_limit (c.whisker_to_cone g).symm, is_colimit := (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g) (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)).symm) (hc.is_colimit.whisker_equivalence (category_theory.discrete.equivalence g))).of_iso_colimit (c.whisker_to_cocone g).symm})
- bicone : category_theory.limits.bicone F
- is_bilimit : self.bicone.is_bilimit
A bicone over F : J → C
, which is both a limit cone and a colimit cocone.
Instances for category_theory.limits.limit_bicone
- category_theory.limits.limit_bicone.has_sizeof_inst
- exists_biproduct : nonempty (category_theory.limits.limit_bicone F)
has_biproduct F
expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram F
.
Use the axiom of choice to extract explicit biproduct_data F
from has_biproduct F
.
A bicone for F
which is both a limit cone and a colimit cocone.
biproduct.bicone F
is a bilimit bicone.
biproduct.bicone F
is a limit cone.
biproduct.bicone F
is a colimit cocone.
- has_biproduct : ∀ (F : J → C), category_theory.limits.has_biproduct F
C
has biproducts of shape J
if we have
a limit and a colimit, with the same cone points,
of every function F : J → C
.
Instances of this typeclass
- has_biproducts_of_shape : ∀ (J : Type) [_inst_3 : 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.
The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.
Equations
- category_theory.limits.biproduct_iso F = (category_theory.limits.limit.is_limit (category_theory.discrete.functor F)).cone_point_unique_up_to_iso (category_theory.limits.biproduct.is_limit F) ≪≫ (category_theory.limits.biproduct.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor F))
biproduct f
computes the biproduct of a family of elements f
. (It is defined as an
abbreviation for limit (discrete.functor f)
, so for most facts about biproduct f
, you will
just use general facts about limits and colimits.)
The projection onto a summand of a biproduct.
The inclusion into a summand of a biproduct.
Note that as this lemma has a if
in the statement, we include a decidable_eq
argument.
This means you may not be able to simp
using this lemma unless you open_locale classical
.
Given a collection of maps into the summands, we obtain a map into the biproduct.
Given a collection of maps out of the summands, we obtain a map out of the biproduct.
Given a collection of maps between corresponding summands of a pair of biproducts indexed by the same type, we obtain a map between the biproducts.
An alternative to biproduct.map
constructed via colimits.
This construction only exists in order to show it is equal to biproduct.map
.
The canonical isomorphism between the chosen biproduct and the chosen product.
The canonical isomorphism between the chosen biproduct and the chosen coproduct.
Given a collection of isomorphisms between corresponding summands of a pair of biproducts indexed by the same type, we obtain an isomorphism between the biproducts.
Equations
- category_theory.limits.biproduct.map_iso p = {hom := category_theory.limits.biproduct.map (λ (b : J), (p b).hom), inv := category_theory.limits.biproduct.map (λ (b : J), (p b).inv), hom_inv_id' := _, inv_hom_id' := _}
The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.
Equations
The canonical morphism from a biproduct to the biproduct over a restriction of its index type.
Equations
The kernel of biproduct.π f i
is the inclusion from the biproduct which omits i
from the index set J
into the biproduct over J
.
Equations
- category_theory.limits.biproduct.is_limit_from_subtype f i = category_theory.limits.fork.is_limit.mk' (category_theory.limits.kernel_fork.of_ι (category_theory.limits.biproduct.from_subtype f (λ (j : J), i ≠ j)) _) (λ (s : category_theory.limits.fork (category_theory.limits.biproduct.π f i) 0), ⟨s.ι ≫ category_theory.limits.biproduct.to_subtype f (λ (j : J), i ≠ j), _⟩)
The cokernel of biproduct.ι f i
is the projection from the biproduct over the index set J
onto the biproduct omitting i
.
Equations
- category_theory.limits.biproduct.is_colimit_to_subtype f i = category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.biproduct.to_subtype f (λ (j : J), i ≠ j)) _) (λ (s : category_theory.limits.cofork (category_theory.limits.biproduct.ι f i) 0), ⟨category_theory.limits.biproduct.from_subtype f (λ (j : J), i ≠ j) ≫ s.π, _⟩)
Convert a (dependently typed) matrix to a morphism of biproducts.
Equations
- category_theory.limits.biproduct.matrix m = category_theory.limits.biproduct.desc (λ (j : J), category_theory.limits.biproduct.lift (λ (k : K), m j k))
Extract the matrix components from a morphism of biproducts.
Equations
Morphisms between direct sums are matrices.
Equations
- category_theory.limits.biproduct.matrix_equiv = {to_fun := category_theory.limits.biproduct.components g, inv_fun := category_theory.limits.biproduct.matrix (λ (k : K), g k), left_inv := _, right_inv := _}
Auxiliary lemma for biproduct.unique_up_to_iso
.
Auxiliary lemma for biproduct.unique_up_to_iso
.
Biproducts are unique up to isomorphism. This already follows because bilimits are limits,
but in the case of biproducts we can give an isomorphism with particularly nice definitional
properties, namely that biproduct.lift b.π
and biproduct.desc b.ι
are inverses of each
other.
Equations
A category with finite biproducts has a zero object.
The limit bicone for the biproduct over an index type with exactly one term.
Equations
- category_theory.limits.limit_bicone_of_unique f = {bicone := {X := f inhabited.default, π := λ (j : J), category_theory.eq_to_hom _, ι := λ (j : J), category_theory.eq_to_hom _, ι_π := _}, is_bilimit := {is_limit := (category_theory.limits.limit_cone_of_unique f).is_limit, is_colimit := (category_theory.limits.colimit_cocone_of_unique f).is_colimit}}
A biproduct over a index type with exactly one term is just the object over that term.
- X : C
- fst : self.X ⟶ P
- snd : self.X ⟶ Q
- inl : P ⟶ self.X
- inr : Q ⟶ self.X
- inl_fst' : self.inl ≫ self.fst = 𝟙 P . "obviously"
- inl_snd' : self.inl ≫ self.snd = 0 . "obviously"
- inr_fst' : self.inr ≫ self.fst = 0 . "obviously"
- inr_snd' : self.inr ≫ self.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
Instances for category_theory.limits.binary_bicone
- category_theory.limits.binary_bicone.has_sizeof_inst
Extract the cone from a binary bicone.
Equations
Extract the cocone from a binary bicone.
Equations
Convert a binary_bicone
into a bicone
over a pair.
A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.
A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit cocone.
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' := _}
A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit cone.
A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a colimit cocone.
- is_limit : category_theory.limits.is_limit b.to_cone
- is_colimit : category_theory.limits.is_colimit b.to_cocone
Structure witnessing that a binary bicone is a limit cone and a limit cocone.
Instances for category_theory.limits.binary_bicone.is_bilimit
- category_theory.limits.binary_bicone.is_bilimit.has_sizeof_inst
A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.
Equations
- b.to_bicone_is_bilimit = {to_fun := λ (h : b.to_bicone.is_bilimit), {is_limit := ⇑(b.to_bicone_is_limit) h.is_limit, is_colimit := ⇑(b.to_bicone_is_colimit) h.is_colimit}, inv_fun := λ (h : b.is_bilimit), {is_limit := ⇑(b.to_bicone_is_limit.symm) h.is_limit, is_colimit := ⇑(b.to_bicone_is_colimit.symm) h.is_colimit}, left_inv := _, right_inv := _}
A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a bilimit.
Equations
- b.to_binary_bicone_is_bilimit = {to_fun := λ (h : b.to_binary_bicone.is_bilimit), {is_limit := ⇑(b.to_binary_bicone_is_limit) h.is_limit, is_colimit := ⇑(b.to_binary_bicone_is_colimit) h.is_colimit}, inv_fun := λ (h : b.is_bilimit), {is_limit := ⇑(b.to_binary_bicone_is_limit.symm) h.is_limit, is_colimit := ⇑(b.to_binary_bicone_is_colimit.symm) h.is_colimit}, left_inv := _, right_inv := _}
- bicone : category_theory.limits.binary_bicone P Q
- is_bilimit : self.bicone.is_bilimit
A bicone over P Q : C
, which is both a limit cone and a colimit cocone.
Instances for category_theory.limits.binary_biproduct_data
- category_theory.limits.binary_biproduct_data.has_sizeof_inst
- exists_binary_biproduct : nonempty (category_theory.limits.binary_biproduct_data P Q)
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
.
Use the axiom of choice to extract explicit binary_biproduct_data F
from has_binary_biproduct F
.
A bicone for P Q
which is both a limit cone and a colimit cocone.
binary_biproduct.bicone P Q
is a limit bicone.
binary_biproduct.bicone P Q
is a limit cone.
binary_biproduct.bicone P Q
is a colimit cocone.
- has_binary_biproduct : ∀ (P Q : C), category_theory.limits.has_binary_biproduct P Q
has_binary_biproducts C
represents the existence of a bicone which is
simultaneously a limit and a colimit of the diagram pair P Q
, for every P Q : C
.
A category with finite biproducts has binary biproducts.
This is not an instance as typically in concrete categories there will be an alternative construction with nicer definitional properties.
The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.
Equations
- category_theory.limits.biprod_iso X Y = (category_theory.limits.limit.is_limit (category_theory.limits.pair X Y)).cone_point_unique_up_to_iso (category_theory.limits.binary_biproduct.is_limit X Y) ≪≫ (category_theory.limits.binary_biproduct.is_colimit X Y).cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit (category_theory.limits.pair X Y))
An arbitrary choice of biproduct of a pair of objects.
The projection onto the first summand of a binary biproduct.
The projection onto the second summand of a binary biproduct.
The inclusion into the first summand of a binary biproduct.
The inclusion into the second summand of a binary biproduct.
Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.
Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.
Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.
An alternative to biprod.map
constructed via colimits.
This construction only exists in order to show it is equal to biprod.map
.
The canonical isomorphism between the chosen biproduct and the chosen product.
The canonical isomorphism between the chosen biproduct and the chosen coproduct.
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' := _}
Auxiliary lemma for biprod.unique_up_to_iso
.
Auxiliary lemma for biprod.unique_up_to_iso
.
Binary biproducts are unique up to isomorphism. This already follows because bilimits are
limits, but in the case of biproducts we can give an isomorphism with particularly nice
definitional properties, namely that biprod.lift b.fst b.snd
and biprod.desc b.inl b.inr
are inverses of each other.
Equations
- category_theory.limits.biprod.unique_up_to_iso X Y hb = {hom := category_theory.limits.biprod.lift b.fst b.snd, inv := category_theory.limits.biprod.desc b.inl b.inr, hom_inv_id' := _, inv_hom_id' := _}
A kernel fork for the kernel of binary_bicone.fst
. It consists of the morphism
binary_bicone.inr
.
Equations
A kernel fork for the kernel of binary_bicone.snd
. It consists of the morphism
binary_bicone.inl
.
Equations
A cokernel cofork for the cokernel of binary_bicone.inl
. It consists of the morphism
binary_bicone.snd
.
Equations
A cokernel cofork for the cokernel of binary_bicone.inr
. It consists of the morphism
binary_bicone.fst
.
Equations
The fork defined in binary_bicone.fst_kernel_fork
is indeed a kernel.
Equations
The fork defined in binary_bicone.snd_kernel_fork
is indeed a kernel.
Equations
The cofork defined in binary_bicone.inl_cokernel_cofork
is indeed a cokernel.
Equations
The cofork defined in binary_bicone.inr_cokernel_cofork
is indeed a cokernel.
Equations
A kernel fork for the kernel of biprod.fst
. It consists of the
morphism biprod.inr
.
The fork biprod.fst_kernel_fork
is indeed a limit.
A kernel fork for the kernel of biprod.snd
. It consists of the
morphism biprod.inl
.
The fork biprod.snd_kernel_fork
is indeed a limit.
A cokernel cofork for the cokernel of biprod.inl
. It consists of the
morphism biprod.snd
.
The cofork biprod.inl_cokernel_fork
is indeed a colimit.
A cokernel cofork for the cokernel of biprod.inr
. It consists of the
morphism biprod.fst
.
The cofork biprod.inr_cokernel_fork
is indeed a colimit.
If Y
is a zero object, X ≅ X ⊞ Y
for any X
.
Equations
- category_theory.limits.iso_biprod_zero hY = {hom := category_theory.limits.biprod.inl _inst_3, inv := category_theory.limits.biprod.fst _inst_3, hom_inv_id' := _, inv_hom_id' := _}
If X
is a zero object, Y ≅ X ⊞ Y
for any Y
.
Equations
- category_theory.limits.iso_zero_biprod hY = {hom := category_theory.limits.biprod.inr _inst_3, inv := category_theory.limits.biprod.snd _inst_3, hom_inv_id' := _, inv_hom_id' := _}
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' := _}
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' := _}
The braiding isomorphism can be passed through a map by swapping the order.
The braiding isomorphism is symmetric.
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.is_bilimit_of_total b total = {is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor f)), finset.univ.sum (λ (j : J), s.π.app {as := 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 {as := j}), fac' := _, uniq' := _}}
In a preadditive category, we can construct a biproduct for f : J → C
from
any bicone b
for f
satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X
.
(That is, such a bicone is a limit cone and a colimit cocone.)
In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.
We can turn any limit cone over a pair into a bilimit bicone.
In a preadditive category, if the product over f : J → C
exists,
then the biproduct over f
exists.
In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.
We can turn any limit cone over a pair into a bilimit bicone.
In a preadditive category, if the coproduct over f : J → C
exists,
then the biproduct over f
exists.
A preadditive category with finite products has finite biproducts.
A preadditive category with finite coproducts has finite biproducts.
In any preadditive category, any biproduct satsifies
∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)
Reindex a categorical biproduct via an equivalence of the index types.
Equations
- category_theory.limits.biproduct.reindex ε f = {hom := category_theory.limits.biproduct.desc (λ (b : β), category_theory.limits.biproduct.ι f (⇑ε b)), inv := category_theory.limits.biproduct.lift (λ (b : β), category_theory.limits.biproduct.π f (⇑ε b)), hom_inv_id' := _, inv_hom_id' := _}
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.is_binary_bilimit_of_total b total = {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' := _}}
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.)
We can turn any limit cone over a pair into a bicone.
Equations
- category_theory.limits.binary_bicone.of_limit_cone ht = {X := t.X, fst := t.π.app {as := category_theory.limits.walking_pair.left}, snd := t.π.app {as := category_theory.limits.walking_pair.right}, inl := ht.lift (category_theory.limits.binary_fan.mk (𝟙 X) 0), inr := ht.lift (category_theory.limits.binary_fan.mk 0 (𝟙 Y)), inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.
We can turn any limit cone over a pair into a bilimit bicone.
In a preadditive category, if the product of X
and Y
exists, then the
binary biproduct of X
and Y
exists.
In a preadditive category, if all binary products exist, then all binary biproducts exist.
We can turn any colimit cocone over a pair into a bicone.
Equations
- category_theory.limits.binary_bicone.of_colimit_cocone ht = {X := t.X, fst := ht.desc (category_theory.limits.binary_cofan.mk (𝟙 X) 0), snd := ht.desc (category_theory.limits.binary_cofan.mk 0 (𝟙 Y)), inl := t.ι.app {as := category_theory.limits.walking_pair.left}, inr := t.ι.app {as := category_theory.limits.walking_pair.right}, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.
We can turn any colimit cocone over a pair into a bilimit bicone.
In a preadditive category, if the coproduct of X
and Y
exists, then the
binary biproduct of X
and Y
exists.
In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.
In any preadditive category, any binary biproduct satsifies
biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)
.
Every split mono f
with a cokernel induces a binary bicone with f
as its inl
and
the cokernel map as its snd
.
We will show in is_bilimit_binary_bicone_of_split_mono_of_cokernel
that this binary bicone is in
fact already a biproduct.
Equations
- category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel i = {X := Y, fst := category_theory.retraction f _inst_5, snd := category_theory.limits.cofork.π c, inl := f, inr := let c' : category_theory.limits.cokernel_cofork (𝟙 Y - (𝟙 Y - category_theory.retraction f ≫ f)) := category_theory.limits.cokernel_cofork.of_π (category_theory.limits.cofork.π c) category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_1, i' : category_theory.limits.is_colimit c' := category_theory.limits.is_cokernel_epi_comp i (category_theory.retraction f) category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_3, i'' : category_theory.limits.is_colimit (category_theory.preadditive.cofork_of_cokernel_cofork c') := category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork i' in (category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork C category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel._proof_4 i'').section_, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
The bicone constructed in binary_bicone_of_split_mono_of_cokernel
is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
If b
is a binary bicone such that b.inl
is a kernel of b.snd
, then b
is a bilimit
bicone.
Equations
- b.is_bilimit_of_kernel_inl hb = category_theory.limits.is_binary_bilimit_of_is_limit b (category_theory.limits.binary_fan.is_limit.mk b.to_cone (λ (T : C) (f : T ⟶ X) (g : T ⟶ Y), f ≫ b.inl + g ≫ b.inr) _ _ _)
If b
is a binary bicone such that b.inr
is a kernel of b.fst
, then b
is a bilimit
bicone.
Equations
- b.is_bilimit_of_kernel_inr hb = category_theory.limits.is_binary_bilimit_of_is_limit b (category_theory.limits.binary_fan.is_limit.mk b.to_cone (λ (T : C) (f : T ⟶ X) (g : T ⟶ Y), f ≫ b.inl + g ≫ b.inr) _ _ _)
If b
is a binary bicone such that b.fst
is a cokernel of b.inr
, then b
is a bilimit
bicone.
Equations
- b.is_bilimit_of_cokernel_fst hb = category_theory.limits.is_binary_bilimit_of_is_colimit b (category_theory.limits.binary_cofan.is_colimit.mk b.to_cocone (λ (T : C) (f : X ⟶ T) (g : Y ⟶ T), b.fst ≫ f + b.snd ≫ g) _ _ _)
If b
is a binary bicone such that b.snd
is a cokernel of b.inl
, then b
is a bilimit
bicone.
Equations
- b.is_bilimit_of_cokernel_snd hb = category_theory.limits.is_binary_bilimit_of_is_colimit b (category_theory.limits.binary_cofan.is_colimit.mk b.to_cocone (λ (T : C) (f : X ⟶ T) (g : Y ⟶ T), b.fst ≫ f + b.snd ≫ g) _ _ _)
Every split epi f
with a kernel induces a binary bicone with f
as its snd
and
the kernel map as its inl
.
We will show in binary_bicone_of_is_split_mono_of_cokernel
that this binary bicone is in fact
already a biproduct.
Equations
- category_theory.limits.binary_bicone_of_is_split_epi_of_kernel i = {X := X, fst := let c' : category_theory.limits.kernel_fork (𝟙 X - (𝟙 X - f ≫ category_theory.section_ f)) := category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι c) category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_1, i' : category_theory.limits.is_limit c' := category_theory.limits.is_kernel_comp_mono i (category_theory.section_ f) category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_3, i'' : category_theory.limits.is_limit (category_theory.preadditive.fork_of_kernel_fork c') := category_theory.preadditive.is_limit_fork_of_kernel_fork i' in (category_theory.limits.split_mono_of_idempotent_of_is_limit_fork C category_theory.limits.binary_bicone_of_is_split_epi_of_kernel._proof_4 i'').retraction, snd := f, inl := category_theory.limits.fork.ι c, inr := category_theory.section_ f _inst_5, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
The bicone constructed in binary_bicone_of_is_split_epi_of_kernel
is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.
The existence of binary biproducts implies that there is at most one preadditive structure.
The existence of binary biproducts implies that there is at most one preadditive structure.
The existence of binary biproducts implies that there is at most one preadditive structure.
An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.
Equations
- category_theory.indecomposable X = (¬category_theory.limits.is_zero X ∧ ∀ (Y Z : C), (X ≅ Y ⊞ Z) → category_theory.limits.is_zero Y ∨ category_theory.limits.is_zero Z)