Structures · Category theory
CategoryTheory.Limits.HasFiniteBiproducts
A category HasFiniteBiproducts if it has a biproduct for every finite family of objects in C
indexed by a finite type.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- ModuleCat
- AddCommGrpCat
- CategoryTheory.Ind
- CategoryTheory.Idempotents.Karoubi
- CategoryTheory.Mat_
- CategoryTheory.InjectiveObject
How is a type an instance?
Loading the hierarchy index…
Assumed by139
- CategoryTheory.Limits.biproduct.matrix
- CategoryTheory.leftDistributor
- CategoryTheory.rightDistributor
- CategoryTheory.Limits.biproduct.matrix_π
- CategoryTheory.Mat_.lift
- CategoryTheory.HomOrthogonal.matrixDecomposition
- CategoryTheory.Limits.biproduct.components
- CategoryTheory.leftDistributor_hom
- CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv
- CategoryTheory.Limits.kernelForkBiproductToSubtype
- CategoryTheory.Idempotents.Karoubi.Biproducts.bicone
- CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype
- CategoryTheory.rightDistributor_hom
- CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts
- CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv
- CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality
- CategoryTheory.Limits.kernelBiproductToSubtypeIso
- CategoryTheory.rightDistributor_ext_left
- CategoryTheory.leftDistributor_inv
- CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op
- CategoryTheory.leftDistributor_ext_left
- CategoryTheory.leftDistributor_ext_right
- CategoryTheory.Mat_.embeddingLiftIso
- CategoryTheory.rightDistributor_inv
- CategoryTheory.Limits.biproduct.matrixEquiv
- CategoryTheory.rightDistributor_hom_comp_biproduct_π
- CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete
- CategoryTheory.HomOrthogonal.matrixDecomposition_apply
- CategoryTheory.Limits.cokernelBiproductFromSubtypeIso
- CategoryTheory.leftDistributor_hom_comp_biproduct_π
- CategoryTheory.rightDistributor_ext_right
- CategoryTheory.Limits.biproduct.matrix_π_assoc
- CategoryTheory.Limits.biproduct.matrix_desc
- CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'
- CategoryTheory.biproduct_ι_comp_rightDistributor_hom
- CategoryTheory.Limits.biproduct.matrix_map
- CategoryTheory.HomOrthogonal.matrixDecomposition_comp
- CategoryTheory.biproduct_ι_comp_leftDistributor_hom
- CategoryTheory.biproduct_ι_comp_leftDistributor_inv
- CategoryTheory.Limits.biproduct.lift_matrix
- CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc
- CategoryTheory.biproduct_ι_comp_rightDistributor_inv
- CategoryTheory.Limits.biproduct.ι_matrix_assoc
- CategoryTheory.rightDistributor_inv_comp_biproduct_π
- CategoryTheory.rightDistributor_ext₂_right
- CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc
- CategoryTheory.Limits.biproduct.map_matrix
- CategoryTheory.leftDistributor_inv_comp_biproduct_π
- CategoryTheory.rightDistributor_ext₂_left
- CategoryTheory.HomOrthogonal.matrixDecomposition_id
Ancestors0
No ancestors.