mathlib documentation

category_theory.limits.preserves.shapes.biproducts

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

The image of a bicone under a functor.

Equations

The image of a binary bicone under a functor.

Equations
@[class]

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
@[class]

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
@[class]

A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a fintype.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_finite_biproducts
  • category_theory.limits.preserves_finite_biproducts.has_sizeof_inst
@[class]

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
@[class]

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
@[class]

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