Preservation of biproducts #
We define the image of a (binary) bicone under a functor that preserves zero morphisms and define
classes preserves_biproduct
and preserves_binary_biproduct
. We then
- show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
- construct the comparison morphisms between the image of a biproduct and the biproduct of the images and show that the biproduct is preserved if one of them is an isomorphism,
- give the canonical isomorphism between the image of a biproduct and the biproduct of the images in case that the biproduct is preserved,
- show that in a preadditive category, a functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.
The image of a bicone under a functor.
The image of a binary bicone under a functor.
- preserves : Π {b : category_theory.limits.bicone f}, b.is_bilimit → (F.map_bicone b).is_bilimit
A functor F
preserves biproducts of f
if F
maps every bilimit bicone over f
to a
bilimit bicone over F.obj ∘ f
.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproduct
- category_theory.limits.preserves_biproduct.has_sizeof_inst
A functor F
preserves biproducts of f
if F
maps every bilimit bicone over f
to a
bilimit bicone over F.obj ∘ f
.
- preserves : Π {f : J → C}, category_theory.limits.preserves_biproduct f F
A functor F
preserves biproducts of shape J
if it preserves biproducts of f
for every
f : J → C
.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproducts_of_shape
- category_theory.limits.preserves_biproducts_of_shape.has_sizeof_inst
- preserves : Π {J : Type} [_inst_5_1 : fintype J], category_theory.limits.preserves_biproducts_of_shape J F
A functor F
preserves finite biproducts if it preserves biproducts of shape J
whenever
J
is a fintype.
Instances of this typeclass
- category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts
- category_theory.functor.preserves_finite_biproducts_of_additive
- category_theory.monoidal_category.tensor_left.limits.preserves_finite_biproducts
- category_theory.monoidal_category.tensor_right.limits.preserves_finite_biproducts
Instances of other typeclasses for category_theory.limits.preserves_finite_biproducts
- category_theory.limits.preserves_finite_biproducts.has_sizeof_inst
- preserves : Π {J : Type ?}, category_theory.limits.preserves_biproducts_of_shape J F
A functor F
preserves biproducts if it preserves biproducts of any shape J
of size w
.
The usual notion of preservation of biproducts is recovered by choosing w
to be the universe
of the morphisms of C
.
Instances for category_theory.limits.preserves_biproducts
- category_theory.limits.preserves_biproducts.has_sizeof_inst
Preserving biproducts at a bigger universe level implies preserving biproducts at a smaller universe level.
Equations
- category_theory.limits.preserves_biproducts_shrink F = {preserves := λ (J : Type w₁), {preserves := λ (f : J → C), {preserves := λ (b : category_theory.limits.bicone f) (ib : b.is_bilimit), ((F.map_bicone b).whisker_is_bilimit_iff equiv.ulift).to_fun (category_theory.limits.is_bilimit_of_preserves F ((b.whisker_is_bilimit_iff equiv.ulift).inv_fun ib))}}}
Equations
- preserves : Π {b : category_theory.limits.binary_bicone X Y}, b.is_bilimit → (F.map_binary_bicone b).is_bilimit
A functor F
preserves binary biproducts of X
and Y
if F
maps every bilimit bicone over
X
and Y
to a bilimit bicone over F.obj X
and F.obj Y
.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_binary_biproduct
- category_theory.limits.preserves_binary_biproduct.has_sizeof_inst
A functor F
preserves binary biproducts of X
and Y
if F
maps every bilimit bicone over
X
and Y
to a bilimit bicone over F.obj X
and F.obj Y
.
- preserves : (Π {X Y : C}, category_theory.limits.preserves_binary_biproduct X Y F) . "apply_instance"
A functor F
preserves binary biproducts if it preserves the binary biproduct of X
and Y
for all X
and Y
.
Instances for category_theory.limits.preserves_binary_biproducts
- category_theory.limits.preserves_binary_biproducts.has_sizeof_inst
A functor that preserves biproducts of a pair preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_biproduct F X Y = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), {is_limit := (⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))) (F.map_bicone b.to_bicone).to_cone).symm) (category_theory.limits.is_bilimit_of_preserves F (⇑(b.to_bicone_is_bilimit.symm) 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.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))).hom).obj (F.map_bicone b.to_bicone).to_cone).X) _), is_colimit := (⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))) (F.map_bicone b.to_bicone).to_cocone).symm) (category_theory.limits.is_bilimit_of_preserves F (⇑(b.to_bicone_is_bilimit.symm) 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.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))).inv).obj (F.map_bicone b.to_bicone).to_cocone).X) _)}}
A functor that preserves biproducts of a pair preserves binary biproducts.
As for products, any functor between categories with biproducts gives rise to a morphism
F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f)
.
Equations
- F.biproduct_comparison f = category_theory.limits.biproduct.lift (λ (j : J), F.map (category_theory.limits.biproduct.π f j))
Instances for category_theory.functor.biproduct_comparison
As for coproducts, any functor between categories with biproducts gives rise to a morphism
⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)
Equations
- F.biproduct_comparison' f = category_theory.limits.biproduct.desc (λ (j : J), F.map (category_theory.limits.biproduct.ι f j))
Instances for category_theory.functor.biproduct_comparison'
The composition in the opposite direction is equal to the identity if and only if F
preserves
the biproduct, see preserves_biproduct_of_mono_biproduct_comparison
.
biproduct_comparison F f
is a split epimorphism.
Equations
- F.split_epi_biproduct_comparison f = {section_ := F.biproduct_comparison' f _inst_6, id' := _}
biproduct_comparison' F f
is a split monomorphism.
Equations
- F.split_mono_biproduct_comparison' f = {retraction := F.biproduct_comparison f _inst_6, id' := _}
If F
preserves a biproduct, we get a definitionally nice isomorphism
F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f)
.
As for products, any functor between categories with binary biproducts gives rise to a
morphism F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y
.
Equations
Instances for category_theory.functor.biprod_comparison
As for coproducts, any functor between categories with binary biproducts gives rise to a
morphism F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)
.
Equations
Instances for category_theory.functor.biprod_comparison'
The composition in the opposite direction is equal to the identity if and only if F
preserves
the biproduct, see preserves_binary_biproduct_of_mono_biprod_comparison
.
biprod_comparison F X Y
is a split epi.
Equations
- F.split_epi_biprod_comparison X Y = {section_ := F.biprod_comparison' X Y _inst_6, id' := _}
biprod_comparison' F X Y
is a split mono.
Equations
- F.split_mono_biprod_comparison' X Y = {retraction := F.biprod_comparison X Y _inst_6, id' := _}
If F
preserves a binary biproduct, we get a definitionally nice isomorphism
F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y
.
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.