Additivity for the comparison map

The two constructions flanking the comparison map of Deligne's (2.11.1) are additive: the tensor product of super modules is additive in each variable, and realization turns a finite sum of endomorphisms of a module object summing to the identity into a finite sum of endomorphisms of its realization summing to the identity. These are what let a decomposition of a module object into a finite family of retracts be pushed through the comparison.

theorem RS.SuperCommAlgebra.Mod.sum_evenMap_apply {S : SuperCommAlgebra} {M N : S.Mod} {ι : Type u_1} (s : Finset ι) (f : ι → (M ⟶ N)) (m : M.even) : (∑ i ∈ s, f i).evenMap m = ∑ i ∈ s, (f i).evenMap m

The even component of a finite sum of morphisms, pointwise.

theorem RS.SuperCommAlgebra.Mod.sum_oddMap_apply {S : SuperCommAlgebra} {M N : S.Mod} {ι : Type u_1} (s : Finset ι) (f : ι → (M ⟶ N)) (m : M.odd) : (∑ i ∈ s, f i).oddMap m = ∑ i ∈ s, (f i).oddMap m

The odd component of a finite sum of morphisms, pointwise.

theorem RS.SuperCommAlgebra.Mod.tensorHom_add_left {S : SuperCommAlgebra} {M N P Q : S.Mod} (f f' : M ⟶ P) (g : N ⟶ Q) : tensorHom (f + f') g = tensorHom f g + tensorHom f' g

The tensor product of super modules is additive in the left variable.

theorem RS.SuperCommAlgebra.Mod.tensorHom_zero_left {S : SuperCommAlgebra} {M N P Q : S.Mod} (g : N ⟶ Q) : tensorHom 0 g = 0

The tensor product of super modules kills the zero morphism in the left variable.

theorem RS.SuperCommAlgebra.Mod.tensorHom_sum_left {S : SuperCommAlgebra} {M N P Q : S.Mod} {ι : Type u_1} (s : Finset ι) (f : ι → (M ⟶ P)) (g : N ⟶ Q) : tensorHom (∑ i ∈ s, f i) g = ∑ i ∈ s, tensorHom (f i) g

The tensor product of super modules takes a finite sum in the left variable to a finite sum.

Additivity of realization

theorem RS.sum_gammaModuleFunctor_map {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] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {P : CategoryTheory.Mod D R} {ι : Type u_1} (s : Finset ι) (g : ι → (P ⟶ P)) (h : ∑ i ∈ s, (g i).hom = CategoryTheory.CategoryStruct.id P.X) : ∑ i ∈ s, (gammaModuleFunctor L R).map (g i) = CategoryTheory.CategoryStruct.id ((gammaModuleFunctor L R).obj P)

Realization is additive on endomorphisms: a finite family of endomorphisms of a module object whose underlying morphisms sum to the identity realizes to a family summing to the identity.