Exactness of componentwise maps on direct sums

A family of exact pairs of module maps induces an exact pair on the external direct sums. This is the algebraic input for taking direct sums of projective resolutions: kernels and ranges of the componentwise maps are themselves computed componentwise.

Main results

• Function.Exact.directSum: componentwise direct sums preserve exact pairs of module maps.

theorem Function.Exact.directSum {R : Type uR} [Semiring R] {ι : Type uι} {M : ι → Type uM} {N : ι → Type uN} {P : ι → Type uP} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → AddCommMonoid (P i)] [(i : ι) → Module R (M i)] [(i : ι) → Module R (N i)] [(i : ι) → Module R (P i)] {f : (i : ι) → M i →ₗ[R] N i} {g : (i : ι) → N i →ₗ[R] P i} (h : ∀ (i : ι), Exact ⇑(f i) ⇑(g i)) : Exact ⇑(DirectSum.lmap f) ⇑(DirectSum.lmap g)

Componentwise direct sums preserve exact pairs of module maps.