Basic facts about biproducts in preadditive categories. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In (or between) preadditive categories,
-
Any biproduct satisfies the equality
total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)
, or, in the binary case,total : fst ≫ inl + snd ≫ inr = 𝟙 X
. -
Any (binary)
product
or (binary)coproduct
is a (binary)biproduct
. -
In any category (with zero morphisms), if
biprod.map f g
is an isomorphism, then bothf
andg
are isomorphisms. -
If
f
is a morphismX₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
whoseX₁ ⟶ Y₁
entry is an isomorphism, then we can construct isomorphismsL : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
andR : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
so thatL.hom ≫ g ≫ R.hom
is diagonal (withX₁ ⟶ Y₁
component stillf
), via Gaussian elimination. -
As a corollary of the previous two facts, if we have an isomorphism
X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
whoseX₁ ⟶ Y₁
entry is an isomorphism, we can construct an isomorphismX₂ ≅ Y₂
. -
If
f : W ⊞ X ⟶ Y ⊞ Z
is an isomorphism, either𝟙 W = 0
, or at least one of the component mapsW ⟶ Y
andW ⟶ Z
is nonzero. -
If
f : ⨁ S ⟶ ⨁ T
is an isomorphism, then every column (corresponding to a nonzero summand in the domain) has some nonzero matrix entry. -
A functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.
There are connections between this material and the special case of the category whose morphisms are
matrices over a ring, in particular the Schur complement (see
linear_algebra.matrix.schur_complement
). In particular, the declarations
category_theory.biprod.iso_elim
, category_theory.biprod.gaussian
and matrix.invertible_of_from_blocks₁₁_invertible
are all closely related.
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.
The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
with specified components.
Equations
- category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ = category_theory.limits.biprod.fst ≫ f₁₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.fst ≫ f₁₂ ≫ category_theory.limits.biprod.inr + category_theory.limits.biprod.snd ≫ f₂₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.snd ≫ f₂₂ ≫ category_theory.limits.biprod.inr
The unipotent upper triangular matrix
(1 r)
(0 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_upper r = {hom := category_theory.biprod.of_components (𝟙 X₁) r 0 (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) (-r) 0 (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
The unipotent lower triangular matrix
(1 0)
(r 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_lower r = {hom := category_theory.biprod.of_components (𝟙 X₁) 0 r (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) 0 (-r) (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
If f
is a morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
whose X₁ ⟶ Y₁
entry is an isomorphism,
then we can construct isomorphisms L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
and R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
so that L.hom ≫ g ≫ R.hom
is diagonal (with X₁ ⟶ Y₁
component still f
),
via Gaussian elimination.
(This is the version of biprod.gaussian
written in terms of components.)
Equations
- category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂ = ⟨category_theory.biprod.unipotent_lower (-f₂₁ ≫ category_theory.inv f₁₁), ⟨category_theory.biprod.unipotent_upper (-category_theory.inv f₁₁ ≫ f₁₂), ⟨f₂₂ - f₂₁ ≫ category_theory.inv f₁₁ ≫ f₁₂, _⟩⟩⟩
If f
is a morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
whose X₁ ⟶ Y₁
entry is an isomorphism,
then we can construct isomorphisms L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
and R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
so that L.hom ≫ g ≫ R.hom
is diagonal (with X₁ ⟶ Y₁
component still f
),
via Gaussian elimination.
Equations
- category_theory.biprod.gaussian f = let this : Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) ≫ R.hom = category_theory.limits.biprod.map (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) g₂₂ := category_theory.biprod.gaussian' (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) in _.mpr (_.mp this)
If X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
via a two-by-two matrix whose X₁ ⟶ Y₁
entry is an isomorphism,
then we can construct an isomorphism X₂ ≅ Y₂
, via Gaussian elimination.
Equations
- category_theory.biprod.iso_elim' f₁₁ f₁₂ f₂₁ f₂₂ = (category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂).cases_on (λ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (snd : Σ' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂), snd.cases_on (λ (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (snd_snd : Σ' (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂), snd_snd.cases_on (λ (g : X₂ ⟶ Y₂) (w : L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g), let _inst : category_theory.is_iso (category_theory.limits.biprod.map f₁₁ g) := _, _inst_6 : category_theory.is_iso g := _ in category_theory.as_iso g)))
If f
is an isomorphism X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
whose X₁ ⟶ Y₁
entry is an isomorphism,
then we can construct an isomorphism X₂ ≅ Y₂
, via Gaussian elimination.
Equations
- category_theory.biprod.iso_elim f = let _inst : category_theory.is_iso (category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)) := _ in category_theory.biprod.iso_elim' (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)
If f : ⨁ S ⟶ ⨁ T
is an isomorphism, and s
is a non-trivial summand of the source,
then there is some t
in the target so that the s, t
matrix entry of f
is nonzero.
Equations
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
Equations
- category_theory.limits.preserves_product_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).X) _)}
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_product F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_limit (F.map_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_cone b.to_cone)).X) _))}
If the (product-like) biproduct comparison for F
and f
is a monomorphism, then F
preserves the biproduct of f
. For the converse, see map_biproduct
.
If the (coproduct-like) biproduct comparison for F
and f
is an epimorphism, then F
preserves the biproduct of F
and f
. For the converse, see map_biproduct
.
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
Equations
- category_theory.limits.preserves_coproduct_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).X) _)}
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_coproduct F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_colimit (F.map_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_cocone b.to_cocone)).X) _))}
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
Equations
- category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).X) _)}
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_limit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_cone b.to_cone)).X) _))}
If the (product-like) biproduct comparison for F
, X
and Y
is a monomorphism, then
F
preserves the biproduct of X
and Y
. For the converse, see map_biprod
.
If the (coproduct-like) biproduct comparison for F
, X
and Y
is an epimorphism, then
F
preserves the biproduct of X
and Y
. For the converse, see map_biprod
.
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
Equations
- category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).X) _)}
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_colimit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_cocone b.to_cocone)).X) _))}
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.