The ind tensor preserves all small colimits #
Combining the finite-colimit half (IndCoeq), the filtered half
(IndTensorExact) and the preservation of coproducts from finite
and filtered (CoprodPreserve): tensoring on either side in the
ind-category preserves every small colimit. This is the form in
which the coend presentations of §3 pass through the tensor
product.
instance
RS.tensorLeft_ind_preservesShapeDiscrete
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Abelian C]
[CategoryTheory.RigidCategory C]
[CategoryTheory.MonoidalPreadditive C]
(A : CategoryTheory.Ind C)
(α : Type v)
:
instance
RS.tensorRight_ind_preservesShapeDiscrete
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Abelian C]
[CategoryTheory.RigidCategory C]
[CategoryTheory.MonoidalPreadditive C]
(A : CategoryTheory.Ind C)
(α : Type v)
:
instance
RS.tensorLeft_ind_preservesColimits
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Abelian C]
[CategoryTheory.RigidCategory C]
[CategoryTheory.MonoidalPreadditive C]
(A : CategoryTheory.Ind C)
:
Tensoring preserves all small colimits in the ind-category, left-hand version.
instance
RS.tensorRight_ind_preservesColimits
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Abelian C]
[CategoryTheory.RigidCategory C]
[CategoryTheory.MonoidalPreadditive C]
(A : CategoryTheory.Ind C)
:
Tensoring preserves all small colimits in the ind-category, right-hand version.