Structures · Category theory
CategoryTheory.Limits.HasBinaryBiproducts
HasBinaryBiproducts C represents the existence of a bicone which is
simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.
- Shape
- One type argument · adds has_binary_biproduct
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.Limits.HasBinaryBiproducts is also a
Concrete types that are instances6
- CategoryTheory.Functor
- ModuleCat
- AddCommGrpCat
- Rep
- CategoryTheory.InjectiveObject
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by244
- CochainComplex.mappingCone.triangle
- CochainComplex.mappingConeCompTriangle
- CochainComplex.mappingCone.map
- CochainComplex.mappingCone.triangleh
- CategoryTheory.Biprod.ofComponents
- CochainComplex.mappingConeCompHomotopyEquiv
- CategoryTheory.Limits.biprod.braiding
- CochainComplex.mappingCone.triangleRotateShortComplex
- CategoryTheory.Limits.pointwiseBinaryBicone
- HomotopyCategory.Pretriangulated.distinguishedTriangles
- CochainComplex.mappingCone.mapOfHomotopy
- CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
- CategoryTheory.Limits.biprod.associator
- CochainComplex.mappingCone.inr_f_triangle_mor₃_f
- CochainComplex.mappingCocone.triangle
- CochainComplex.mappingConeHomOfDegreewiseSplitIso
- CochainComplex.mappingCone.inl_v_triangle_mor₃_f
- CochainComplex.mappingCone.trianglehMapOfHomotopy
- CategoryTheory.Limits.biprod.braiding_hom
- CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts
- CochainComplex.mappingCone.triangleRotateShortComplexSplitting
- HomotopyCategory.composableArrowsFunctor
- CochainComplex.mappingCone.triangleMap
- CochainComplex.mappingCone.rotateHomotopyEquiv
- CochainComplex.mappingConeHomOfDegreewiseSplitXIso
- CochainComplex.mappingConeCompTriangleh
- CategoryTheory.Limits.biprod.braiding'
- CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc
- CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd
- CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc
- CategoryTheory.Biprod.unipotentUpper
- CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd
- CochainComplex.mappingConeCompHomotopyEquiv_comm₁
- CategoryTheory.AdditiveFunctor.ofRightExact
- CategoryTheory.AdditiveFunctor.ofExact
- HomotopyCategory.Pretriangulated.rotate_distinguished_triangle'
- CochainComplex.mappingConeCompHomotopyEquiv_comm₂
- CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id
- CochainComplex.MappingConeCompHomotopyEquiv.hom
- CategoryTheory.Biprod.unipotentLower
- CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels
- CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel
- CochainComplex.mappingConeCompTriangleh_comm₁
- CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels
- HomotopyCategory.Pretriangulated.isomorphic_distinguished
- HomotopyCategory.spectralObjectMappingCone
- CategoryTheory.Preadditive.RightFreyd.Candidate.desc
- CategoryTheory.AdditiveFunctor.ofLeftExact
- CategoryTheory.Preadditive.RightFreyd.Candidate.π