The comparison map on a family of retracts

If a module object is presented as a finite family of retracts whose projectors sum to the identity, and the comparison map of Deligne's (2.11.1) is invertible on each retract, then it is invertible on the module object itself. This is the additivity step that reduces (2.11.1) on free modules to the two rank-one cases; it needs no biproducts in the category of module objects, only the retraction identities and the totality of the projectors.

theorem RS.sum_modTensorMapMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {ι : Type u_1} (s : Finset ι) {M N : CategoryTheory.Mod D R} (g : ι → (M ⟶ M)) (h : ∑ i ∈ s, (g i).hom = CategoryTheory.CategoryStruct.id M.X) : ∑ i ∈ s, (modTensorMapMod R (g i) (CategoryTheory.CategoryStruct.id N)).hom = CategoryTheory.CategoryStruct.id (modTensorMod R M N).X

A finite family of endomorphisms of a module object whose underlying morphisms sum to the identity stays total after tensoring with a second module object.

theorem RS.isIso_gammaPairComparison_of_retracts {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {ι : Type u_1} [Fintype ι] {M : CategoryTheory.Mod D R} {M' : ι → CategoryTheory.Mod D R} (N : CategoryTheory.Mod D R) (s : (i : ι) → M' i ⟶ M) (r : (i : ι) → M ⟶ M' i) (htot : ∑ i : ι, CategoryTheory.CategoryStruct.comp (r i).hom (s i).hom = CategoryTheory.CategoryStruct.id M.X) (h : ∀ (i : ι), CategoryTheory.IsIso (gammaPairComparison L R (M' i) N)) : CategoryTheory.IsIso (gammaPairComparison L R M N)

The comparison map on a family of retracts.