Structures · Category theory
CategoryTheory.Limits.PreservesBinaryBiproduct
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.
- Shape
- 3 explicit arguments · adds preserves
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- HomologicalComplex
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CategoryTheory.Functor.mapBiprod
- CategoryTheory.Limits.isBinaryBilimitOfPreserves
- CategoryTheory.Limits.biprod.lift_mapBiprod
- CategoryTheory.Limits.biprod.mapBiprod_hom_desc
- CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc
- CategoryTheory.Limits.biprod.map_lift_mapBiprod
- CategoryTheory.Limits.PreservesBinaryBiproduct.preserves
- CategoryTheory.Limits.isBinaryBilimitOfPreserves.congr_simp
- CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct
- CategoryTheory.Functor.mapBiprod_hom
- CategoryTheory.Functor.hasBinaryBiproduct_of_preserves
- CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct
- CategoryTheory.Functor.mapBiprod_inv
Ancestors0
No ancestors.