Function.LinearMap.exact_iff

theorem Function.LinearMap.exact_iff : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g ↔ LinearMap.ker g = LinearMap.range f

This theorem states that for any three types `M`, `N`, and `P` and a type `R` with a commutative semiring structure, and given additive commutative monoid structures on `M`, `N`, and `P`, as well as `R`-module structures on `M`, `N`, and `P`, for any linear maps `f` from `M` to `N` and `g` from `N` to `P`, the maps `f` and `g` form an exact pair if and only if the kernel of `g` is equal to the range of `f`. Here, an exact pair of maps means that for any element `y` from `N`, `g` of `y` equals to zero if and only if `y` is in the image of `f`.

More concisely: Given commutative semirings R, types M, N, P with additive commutative monoid and R-module structures, maps f : M -> N and g : N -> P are exact pairs if and only if the kernel of g equals the range of f.