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]
structure category_theory.limits.preserves_biproduct {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_morphisms D] {J : Type w₁} (f : J → C) (F : C D) [F.preserves_zero_morphisms] :
Type (max u₁ u₂ v₁ v₂ w₁)

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.

Equations
@[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 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
@[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

As for products, any functor between categories with biproducts gives rise to a morphism F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f).

Equations
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
Instances for category_theory.functor.biproduct_comparison'
@[simp]

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.

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'
@[simp]

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.