Structures · Category theory
CategoryTheory.Limits.HasBinaryBiproduct
HasBinaryBiproduct P Q expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram pair P Q.
- Shape
- 2 explicit arguments · adds exists_binary_biproduct
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances3
- HomologicalComplex
- CategoryTheory.Idempotents.Karoubi
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by360
- CategoryTheory.Limits.biprod
- CategoryTheory.Limits.biprod.snd
- CategoryTheory.Limits.biprod.inl
- CategoryTheory.Limits.biprod.fst
- CategoryTheory.Limits.biprod.inr
- CategoryTheory.Limits.biprod.lift
- CategoryTheory.Limits.BinaryBiproduct.bicone
- CategoryTheory.Limits.biprod.desc
- CategoryTheory.Limits.biprod.hom_ext
- CategoryTheory.Limits.biprod.lift_snd
- HomologicalComplex.cylinder
- CategoryTheory.Limits.biprod.lift_fst
- CategoryTheory.Limits.biprod.hom_ext'
- HomologicalComplex.HasCylinder
- CategoryTheory.Limits.biprod.map
- HomologicalComplex.HasPathObject
- HomologicalComplex.pathObject
- HomologicalComplex.homotopyCofiber.XIsoBiprod
- CategoryTheory.Limits.biprod.inl_desc
- CategoryTheory.Limits.biprod.inr_desc
- HomologicalComplex.cylinder.π
- CategoryTheory.Limits.biprod.opIso
- HomologicalComplex.cylinder.ι₀
- CategoryTheory.Limits.BinaryBiproduct.isLimit
- CategoryTheory.Pretriangulated.binaryBiproductTriangle
- CategoryTheory.Functor.mapBiprod
- CategoryTheory.Limits.BinaryBiproduct.isBilimit
- CategoryTheory.Functor.biprodComparison
- HomologicalComplex.pathObject.π₀
- CategoryTheory.CommSq.shortComplex
- HomologicalComplex.cylinder.ι₁
- CategoryTheory.Functor.biprodComparison'
- HomologicalComplex.biprodXIso
- HomologicalComplex.pathObject.ι
- CategoryTheory.Limits.BinaryBiproduct.isColimit
- CategoryTheory.Limits.biprod.inr_desc_assoc
- CategoryTheory.Limits.biprod.lift_desc
- CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle
- HomologicalComplex.pathObject.π₁
- CategoryTheory.CommSq.shortComplex'
- CategoryTheory.Limits.biprod.inl_desc_assoc
- CategoryTheory.Limits.biprod.map_fst
- HomologicalComplex.cylinder.inlX
- CategoryTheory.Limits.biprod.inl_fst
- HomologicalComplex.cylinder.homotopyEquiv
- HomologicalComplex.cylinder.desc
- HomologicalComplex.cylinder.mapHomologicalComplexObjIso
- CategoryTheory.Limits.biprod.map_snd
- CategoryTheory.Limits.getBinaryBiproductData
- HomologicalComplex.pathObject.mapHomologicalComplexObjIso
Ancestors0
No ancestors.