theorem DirectLimitExact.directLimit_map_exact {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] {G : ι → Type u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {G' : ι → Type u_4} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} [DirectedSystem G' fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)] {G'' : ι → Type u_5} [(i : ι) → AddCommGroup (G'' i)] [(i : ι) → Module R (G'' i)] {f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j} [DirectedSystem G'' fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f'' x1 x2 x3)] (p : (i : ι) → G i →ₗ[R] G' i) (hp : ∀ (i j : ι) (h : i ≤ j), p j ∘ₗ f i j h = f' i j h ∘ₗ p i) (q : (i : ι) → G' i →ₗ[R] G'' i) (hq : ∀ (i j : ι) (h : i ≤ j), q j ∘ₗ f' i j h = f'' i j h ∘ₗ q i) (exact_at : ∀ (i : ι), Function.Exact ⇑(p i) ⇑(q i)) : Function.Exact ⇑(Module.DirectLimit.map p hp) ⇑(Module.DirectLimit.map q hq)

Proposition 23.12 (module version). Exactness of the direct limit functor on modules: given a directed system of short exact sequences $$G' \xrightarrow{p} G \xrightarrow{q} G''$$ of $R$-modules whose squares commute with the structure maps, the induced sequence $$\varinjlim G' \xrightarrow{\varinjlim p} \varinjlim G \xrightarrow{\varinjlim q} \varinjlim G''$$ is exact.