Exactness of the tensor product on ind-objects, (co)equalizer half

Deligne's 2.2, finite-(co)limit half: for a small rigid abelian monoidal C with preadditive tensor, the transported tensor product of Ind C preserves finite colimits and finite limits in each variable. This closes the gap documented in RS.Classical.Deligne.IndTensorExact, whose additivity results cover the finite-(co)product halves; what remains, and is proved here, is preservation of coequalizers and of equalizers.

The route is a two-stage descent from the exactness of the tensor of C itself (RS.Classical.Deligne.TensorExact):

• Embedded stage (RS.preservesColimit_parallelPair_tensorLeft_indOf and its limit and right-hand twins): a parallel pair of Ind C is presented as a filtered colimit of parallel pairs of C (Mathlib's IndParallelPairPresentation), i.e. the pair is isomorphic to parallelPair φ ψ ⋙ Ind.lim I. Tensoring by an embedded object commutes with Ind.lim up to the natural isomorphism RS.indLimCompTensorLeftIso, built from RS.indOfTensorIso and its naturality; on the functor category side the whiskered tensorLeft a preserves (co)equalizers pointwise because tensorLeft a preserves all (co)limits in the rigid C, and Ind.lim preserves finite limits and colimits. Preservation transports along the presentation.
• Descent stage (RS.isIso_post_parallelPair_tensorLeft, RS.isIso_limitPost_parallelPair_tensorLeft and twins): for a fixed parallel pair, the (co)limit comparison of tensorLeft A is natural in the tensoring object A (RS.whiskerLeftCoeqComparison/RS.whiskerLeftEqComparison), between endofunctor-composites that preserve filtered colimits. The filtered-descent lemma RS.isIso_app_of_isIso_indOf of IndTensorExact then propagates invertibility from the embedded stage to every A : Ind C. For coequalizers the required filtered preservation of colim-composites is formal; for equalizers it is the exactness of filtered colimits in Ind C, derived here as RS.preservesColimitsOfShape_parallelPairLim_ind from the type-level commutation of filtered colimits with finite limits through the interchange transpose RS.preservesColimitsOfShape_lim and the inclusion into presheaves.

Deliverables, for every A : Ind C:

• RS.tensorLeft_ind_preservesCoequalizers / RS.tensorRight_ind_preservesCoequalizers and RS.tensorLeft_ind_preservesEqualizers / RS.tensorRight_ind_preservesEqualizers — preservation of WalkingParallelPair colimits and limits for both tensoring functors;
• RS.tensorLeft_ind_preservesFiniteColimits / RS.tensorRight_ind_preservesFiniteColimits — the tensor of Ind C is right exact in each variable;
• RS.tensorLeft_ind_preservesFiniteLimits / RS.tensorRight_ind_preservesFiniteLimits — and left exact, combining with the additivity of IndTensorExact.

The acceptance tests confirm that the cokernel and kernel comparison isomorphisms of both tensoring functors synthesize.

theorem RS.preservesColimit_comp_diagram {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] {𝒜 : Type w₃} [CategoryTheory.Category.{w₄, w₃} 𝒜] {ℬ : Type w₅} [CategoryTheory.Category.{w₆, w₅} ℬ] {𝒞 : Type w₇} [CategoryTheory.Category.{w₈, w₇} 𝒞] (K : CategoryTheory.Functor J 𝒜) (F : CategoryTheory.Functor 𝒜 ℬ) (T : CategoryTheory.Functor ℬ 𝒞) [CategoryTheory.Limits.HasColimit K] [CategoryTheory.Limits.PreservesColimit K F] [CategoryTheory.Limits.PreservesColimit K (F.comp T)] : CategoryTheory.Limits.PreservesColimit (K.comp F) T

Preservation of the colimit of a composed diagram K ⋙ F by T, given that F preserves the colimit of K and the composite functor F ⋙ T does: the colimit cocone of K ⋙ F may be taken to be the image under F of the colimit cocone of K.

theorem RS.preservesLimit_comp_diagram {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] {𝒜 : Type w₃} [CategoryTheory.Category.{w₄, w₃} 𝒜] {ℬ : Type w₅} [CategoryTheory.Category.{w₆, w₅} ℬ] {𝒞 : Type w₇} [CategoryTheory.Category.{w₈, w₇} 𝒞] (K : CategoryTheory.Functor J 𝒜) (F : CategoryTheory.Functor 𝒜 ℬ) (T : CategoryTheory.Functor ℬ 𝒞) [CategoryTheory.Limits.HasLimit K] [CategoryTheory.Limits.PreservesLimit K F] [CategoryTheory.Limits.PreservesLimit K (F.comp T)] : CategoryTheory.Limits.PreservesLimit (K.comp F) T

Dual of RS.preservesColimit_comp_diagram.

theorem RS.preservesColimit_flip_lim {J : Type x₁} [CategoryTheory.Category.{x₂, x₁} J] {K : Type x₃} [CategoryTheory.Category.{x₄, x₃} K] {𝒟 : Type x₅} [CategoryTheory.Category.{x₆, x₅} 𝒟] [CategoryTheory.Limits.HasLimitsOfShape J 𝒟] [CategoryTheory.Limits.HasColimitsOfShape K 𝒟] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (G : CategoryTheory.Functor J (CategoryTheory.Functor K 𝒟)) : CategoryTheory.Limits.PreservesColimit G.flip CategoryTheory.Limits.lim

Transpose of the interchange property, flipped-diagram form: if K-indexed colimits preserve J-limits, the J-limit functor preserves the colimit of G.flip for any bifunctor G. The colimit comparison is identified with the canonical interchange isomorphism Limits.colimitLimitIso.

theorem RS.preservesColimitsOfShape_lim {J : Type x₁} [CategoryTheory.Category.{x₂, x₁} J] {K : Type x₃} [CategoryTheory.Category.{x₄, x₃} K] {𝒟 : Type x₅} [CategoryTheory.Category.{x₆, x₅} 𝒟] [CategoryTheory.Limits.HasLimitsOfShape J 𝒟] [CategoryTheory.Limits.HasColimitsOfShape K 𝒟] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.PreservesColimitsOfShape K CategoryTheory.Limits.lim

Transpose of the interchange property: if K-indexed colimits preserve J-limits, then the J-limit functor preserves K-colimits.

noncomputable def RS.indOfCompTensorLeftIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (a : C) : indOf.comp (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a)) ≅ (CategoryTheory.MonoidalCategory.tensorLeft a).comp indOf

The embedding-tensor comparison as a natural isomorphism, left version: composing the embedding with left tensoring by an embedded object is left tensoring in C followed by the embedding.

Equations

• RS.indOfCompTensorLeftIso a = CategoryTheory.NatIso.ofComponents (fun (x : C) => RS.indOfTensorIso a x) ⋯

noncomputable def RS.indOfCompTensorRightIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (a : C) : indOf.comp (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a)) ≅ (CategoryTheory.MonoidalCategory.tensorRight a).comp indOf

The embedding-tensor comparison as a natural isomorphism, right version.

Equations

• RS.indOfCompTensorRightIso a = CategoryTheory.NatIso.ofComponents (fun (x : C) => RS.indOfTensorIso x a) ⋯

noncomputable def RS.indLimCompTensorLeftIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (a : C) (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : (CategoryTheory.Ind.lim I).comp (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a)) ≅ ((CategoryTheory.Functor.whiskeringRight I C C).obj (CategoryTheory.MonoidalCategory.tensorLeft a)).comp (CategoryTheory.Ind.lim I)

Left tensoring by an embedded object commutes with Ind.lim: the composite Ind.lim I ⋙ tensorLeft (indOf.obj a) is the whiskering of tensorLeft a followed by Ind.lim I. The chain mirrors Mathlib's Ind.limCompInclusion, with the embedded-tensor isomorphism in place of Ind.yonedaCompInclusion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.indLimCompTensorRightIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (a : C) (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : (CategoryTheory.Ind.lim I).comp (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a)) ≅ ((CategoryTheory.Functor.whiskeringRight I C C).obj (CategoryTheory.MonoidalCategory.tensorRight a)).comp (CategoryTheory.Ind.lim I)

Right tensoring by an embedded object commutes with Ind.lim.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.preservesColimit_parallelPair_tensorLeft_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (a : C) {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a))

Embedded stage, left version: left tensoring by an embedded object preserves the colimit of every parallel pair of Ind C. The pair is presented as a filtered colimit of parallel pairs of C; tensoring commutes with the presentation by RS.indLimCompTensorLeftIso, and on the functor-category side the whiskered tensorLeft a preserves coequalizers pointwise since the tensor of the rigid C is exact.

theorem RS.preservesLimit_parallelPair_tensorLeft_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (a : C) {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a))

Embedded stage for limits, left version: left tensoring by an embedded object preserves the limit of every parallel pair of Ind C — the dual of the coequalizer argument, using that Ind.lim preserves finite limits and that the tensor of the rigid C is left exact.

theorem RS.preservesLimit_parallelPair_tensorRight_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (a : C) {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a))

Embedded stage for limits, right version.

theorem RS.preservesColimit_parallelPair_tensorRight_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (a : C) {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a))

Embedded stage, right version.

@[reducible]

noncomputable def RS.whiskerLeftPairFunctor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C))

The parallel pair (A ◁ f, A ◁ g) as a functor of the tensoring object A. The @[reducible] marking is deliberate: the object field must reduce at instance transparency for the show-retyped colimit proofs below to be stateable.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

noncomputable def RS.whiskerRightPairFunctor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C))

The parallel pair (f ▷ A, g ▷ A) as a functor of the tensoring object A.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.whiskerLeftPairFunctorEvalIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) (k : CategoryTheory.Limits.WalkingParallelPair) : (whiskerLeftPairFunctor f g).comp ((CategoryTheory.evaluation CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C)).obj k) ≅ CategoryTheory.MonoidalCategory.tensorRight ((CategoryTheory.Limits.parallelPair f g).obj k)

Evaluating RS.whiskerLeftPairFunctor at a stage of the walking parallel pair gives right tensoring by the corresponding object.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.whiskerRightPairFunctorEvalIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) (k : CategoryTheory.Limits.WalkingParallelPair) : (whiskerRightPairFunctor f g).comp ((CategoryTheory.evaluation CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C)).obj k) ≅ CategoryTheory.MonoidalCategory.tensorLeft ((CategoryTheory.Limits.parallelPair f g).obj k)

Evaluating RS.whiskerRightPairFunctor at a stage gives left tensoring by the corresponding object.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.preservesFilteredColimits_whiskerLeftPairFunctor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesFilteredColimits (whiskerLeftPairFunctor f g)

The pair functor preserves filtered colimits, pointwise.

theorem RS.preservesFilteredColimits_whiskerRightPairFunctor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.Limits.PreservesFilteredColimits (whiskerRightPairFunctor f g)

The right-hand pair functor preserves filtered colimits.

noncomputable def RS.whiskerLeftCoeqComparison {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : (whiskerLeftPairFunctor f g).comp CategoryTheory.Limits.colim ⟶ CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair f g))

The coequalizer comparison for left tensoring, naturally in the tensoring object: at A it is the canonical morphism from the colimit of the pair (A ◁ f, A ◁ g) to A ⊗ coeq (f, g).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.whiskerRightCoeqComparison {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : (whiskerRightPairFunctor f g).comp CategoryTheory.Limits.colim ⟶ CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair f g))

The coequalizer comparison for right tensoring, naturally in the tensoring object.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.isIso_post_parallelPair_tensorLeft {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] {X Y : CategoryTheory.Ind C} (A : CategoryTheory.Ind C) (f g : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorLeft A))

Descent stage, left version: the colimit comparison of any parallel pair under left tensoring is invertible, for every tensoring ind-object. Filtered descent from the embedded stage.

theorem RS.isIso_post_parallelPair_tensorRight {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] {X Y : CategoryTheory.Ind C} (A : CategoryTheory.Ind C) (f g : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorRight A))

Descent stage, right version.

instance RS.tensorLeft_ind_preservesCoequalizers {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft A)

Left tensoring on Ind C preserves coequalizers.

instance RS.tensorRight_ind_preservesCoequalizers {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight A)

Right tensoring on Ind C preserves coequalizers.

theorem RS.preservesColimitsOfShape_parallelPairLim_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.PreservesColimitsOfShape I CategoryTheory.Limits.lim

Filtered colimits commute with WalkingParallelPair-limits in Ind C: the parallel-pair limit functor preserves filtered colimits. The property holds for types, lifts to presheaves pointwise, transposes through RS.preservesColimitsOfShape_lim, and transports to Ind C along the inclusion, which creates the limits and preserves the filtered colimits involved.

noncomputable def RS.whiskerLeftEqComparison {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.Limits.limit (CategoryTheory.Limits.parallelPair f g)) ⟶ (whiskerLeftPairFunctor f g).comp CategoryTheory.Limits.lim

The equalizer comparison for left tensoring, naturally in the tensoring object: at A it is the canonical morphism from A ⊗ lim (f, g) to the limit of the pair (A ◁ f, A ◁ g).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.whiskerRightEqComparison {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (f g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.Limits.limit (CategoryTheory.Limits.parallelPair f g)) ⟶ (whiskerRightPairFunctor f g).comp CategoryTheory.Limits.lim

The equalizer comparison for right tensoring, naturally in the tensoring object.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.isIso_limitPost_parallelPair_tensorLeft {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] {X Y : CategoryTheory.Ind C} (A : CategoryTheory.Ind C) (f g : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Limits.limit.post (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorLeft A))

Descent stage for limits, left version: the limit comparison of any parallel pair under left tensoring is invertible, for every tensoring ind-object.

theorem RS.isIso_limitPost_parallelPair_tensorRight {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] {X Y : CategoryTheory.Ind C} (A : CategoryTheory.Ind C) (f g : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Limits.limit.post (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.MonoidalCategory.tensorRight A))

Descent stage for limits, right version.

instance RS.tensorLeft_ind_preservesEqualizers {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft A)

Left tensoring on Ind C preserves equalizers.

instance RS.tensorRight_ind_preservesEqualizers {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight A)

Right tensoring on Ind C preserves equalizers.

instance RS.tensorLeft_ind_preservesFiniteColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft A)

Deligne 2.2, right-exactness, left version: left tensoring on Ind C preserves finite colimits — coequalizers by the descent above, finite coproducts by the additivity of RS.Classical.Deligne.IndTensorExact.

instance RS.tensorRight_ind_preservesFiniteColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorRight A)

Deligne 2.2, right-exactness, right version.

instance RS.tensorLeft_ind_preservesFiniteLimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft A)

Left-exactness, left version: left tensoring on Ind C preserves finite limits — equalizers by the dual descent, finite products by additivity. With the right-exactness above, the tensor of Ind C is exact in each variable.

instance RS.tensorRight_ind_preservesFiniteLimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorRight A)

Left-exactness, right version.