The Left Exactness of Hom

If M1 → M2 → M3 → 0 is an exact sequence of R-modules and N is a R-module, then 0 → (M3 →ₗ[R] N) → (M2 →ₗ[R] N) → (M1 →ₗ[R] N) is exact. In this file, we show the exactness at M2 →ₗ[R] N (exact_lcomp_of_exact_of_surjective); the injectivity part is LinearMap.lcomp_injective_of_surjective in the file Mathlib.LinearAlgebra.BilinearMap.

theorem LinearMap.exact_lcomp_of_exact_of_surjective {R : Type u_1} [CommRing R] {M1 : Type u_2} {M2 : Type u_3} {M3 : Type u_4} (N : Type u_5) [AddCommGroup M1] [AddCommGroup M2] [AddCommGroup M3] [AddCommGroup N] [Module R M1] [Module R M2] [Module R M3] [Module R N] {f : M1 →ₗ[R] M2} {g : M2 →ₗ[R] M3} (exac : Function.Exact ⇑f ⇑g) (surj : Function.Surjective ⇑g) : Function.Exact ⇑(lcomp R N g) ⇑(lcomp R N f)