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,
- give the canonical isomorphism between the image of a biproduct and the biproduct of the images,
- 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 (small) shape J
.
Instances for category_theory.limits.preserves_biproducts
- category_theory.limits.preserves_biproducts.has_sizeof_inst
Equations
- category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts F = {preserves := λ (J : Type v) (_x : fintype J), infer_instance}
- 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.
If F
preserves a biproduct, we get a definitionally nice isomorphism
F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f)
.
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) _))}
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) _))}
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.