Pointwise exactness for module-valued functors

Exactness in a functor category is detected by evaluation. This file records the resulting concrete criterion for short complexes of module-valued functors: equality of the image and kernel at every object implies categorical exactness of the natural transformations.

theorem MagnitudeConjecture.CategoryTheory.moduleFunctor_exact_of_app_range_eq_ker {R : Type w} [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor C (ModuleCat R))) (h : ∀ (X : C), (ModuleCat.Hom.hom (S.f.app X)).range = (ModuleCat.Hom.hom (S.g.app X)).ker) : S.Exact

A short complex of module-valued functors is exact when its evaluated linear maps have image equal to kernel at every object.