Structures · Category theory
CategoryTheory.MonoidalPreadditive
A category is MonoidalPreadditive if tensoring is additive in both factors.
Note we don't extend Preadditive C here, as Abelian C already extends it,
and we'll need to have both typeclasses sometimes.
- Shape
- One type argument · adds whiskerLeft_zero, zero_whiskerRight, whiskerLeft_add, add_whiskerRight
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- ModuleCat
- Action
- CategoryTheory.ObjectProperty.FullSubcategory
- Rep
How is a type an instance?
Loading the hierarchy index…
Assumed by88
- CategoryTheory.leftDistributor
- CategoryTheory.rightDistributor
- CategoryTheory.MonoidalPreadditive.zero_whiskerRight
- CategoryTheory.MonoidalPreadditive.whiskerLeft_zero
- CategoryTheory.leftDistributor_hom
- CategoryTheory.Tor'
- CategoryTheory.rightDistributor_hom
- CategoryTheory.Tor
- CategoryTheory.rightDistributor_ext_left
- CategoryTheory.leftDistributor_inv
- CategoryTheory.leftDistributor_ext_left
- CategoryTheory.MonoidalPreadditive.whiskerLeft_add
- CategoryTheory.leftDistributor_ext_right
- CategoryTheory.tensor_sum
- CategoryTheory.rightDistributor_inv
- CategoryTheory.rightDistributor_hom_comp_biproduct_π
- CategoryTheory.MonoidalPreadditive.add_whiskerRight
- CategoryTheory.leftDistributor_hom_comp_biproduct_π
- CategoryTheory.sum_tensor
- CategoryTheory.rightDistributor_ext_right
- CategoryTheory.biproduct_ι_comp_rightDistributor_hom
- CategoryTheory.biproduct_ι_comp_leftDistributor_hom
- CategoryTheory.biproduct_ι_comp_leftDistributor_inv
- CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc
- CategoryTheory.whiskerLeft_sum
- CategoryTheory.biproduct_ι_comp_rightDistributor_inv
- CategoryTheory.rightDistributor_inv_comp_biproduct_π
- CategoryTheory.sum_whiskerRight
- CategoryTheory.rightDistributor_ext₂_right
- CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc
- CategoryTheory.leftDistributor_inv_comp_biproduct_π
- CategoryTheory.rightDistributor_ext₂_left
- CategoryTheory.leftDistributor_ext₂_right
- CategoryTheory.leftDistributor_ext₂_left
- CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory
- CategoryTheory.tensoringRight_linear
- CategoryTheory.rightDistributor_assoc
- CategoryTheory.MonoidalPreadditive.zero_tensor
- CategoryTheory.leftDistributor_assoc
- CategoryTheory.Limits.CokernelCofork.isColimitTensor
- CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory
- CategoryTheory.IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts
- CategoryTheory.tensoringLeft_additive
- CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc
- CategoryTheory.leftDistributor_ext₂_left_iff
- CategoryTheory.MonoidalPreadditive.tensor_zero
- CategoryTheory.rightDistributor_ext₂_right_iff
- CategoryTheory.rightDistributor_ext₂_left_iff
- CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc
- CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc
Ancestors0
No ancestors.