Structures · Category theory
CategoryTheory.Limits.PreservesBiproduct
A functor F preserves biproducts of f if F maps every bilimit bicone over f to a
bilimit bicone over F.obj ∘ f.
- Shape
- 2 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 instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CategoryTheory.Functor.mapBiproduct
- CategoryTheory.Limits.isBilimitOfPreserves
- CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct
- CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc
- CategoryTheory.Limits.preservesProduct_of_preservesBiproduct
- CategoryTheory.Limits.biproduct.map_lift_mapBiprod
- CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct
- CategoryTheory.Functor.mapBiproduct_hom
- CategoryTheory.Limits.PreservesBiproduct.preserves
- CategoryTheory.Functor.mapBiproduct_inv
- CategoryTheory.Functor.hasBiproduct_of_preserves'
- CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc
- CategoryTheory.Functor.hasBiproduct_of_preserves
Ancestors0
No ancestors.