theorem TensorProductsAndTor.tensor_right_exact {R : Type u_1} [CommRing R] {N' : Type u_2} {N : Type u_3} {N'' : Type u_4} [AddCommGroup N'] [AddCommGroup N] [AddCommGroup N''] [Module R N'] [Module R N] [Module R N''] (M : Type u_5) [AddCommGroup M] [Module R M] (f : N' →ₗ[R] N) (g : N →ₗ[R] N'') (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g) ∧ Function.Surjective ⇑(LinearMap.lTensor M g)

Proposition 21.1 (Right exactness of tensor product). Tensoring a short exact sequence N' → N → N'' → 0 of R-modules on the left by a fixed module M preserves exactness at N and surjectivity at N''. That is, the sequence M ⊗ N' → M ⊗ N → M ⊗ N'' → 0 is exact. Tensor product is right exact but in general not left exact, which motivates the definition of Tor.

theorem TensorProductsAndTor.directSum_exact {R : Type u_1} [Semiring R] {ι : Type u_2} {M' : ι → Type u_3} [(i : ι) → AddCommMonoid (M' i)] [(i : ι) → Module R (M' i)] {M : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {M'' : ι → Type u_5} [(i : ι) → AddCommMonoid (M'' i)] [(i : ι) → Module R (M'' i)] (f : (i : ι) → M' i →ₗ[R] M i) (g : (i : ι) → M i →ₗ[R] M'' i) (hexact : ∀ (i : ι), Function.Exact ⇑(f i) ⇑(g i)) : Function.Exact ⇑(DirectSum.lmap f) ⇑(DirectSum.lmap g)

Lemma 21.2 (Exactness of direct sums). A family of sequences M' i → M i → M'' i is exact at each index i if and only if the direct-sum sequence ⨁ M' i → ⨁ M i → ⨁ M'' i is exact. This formalizes the statement that direct sums of modules commute with taking homology/exactness; it is the key fact used to compute Tor of a direct sum as a direct sum of Tor's.