Finiteness consequences of exact sequences

This file records two elementary consequences of exactness at the middle term: finite-dimensional outer vector spaces (over a division ring) force the middle vector space to be finite-dimensional, and trivial outer types force the middle type to be trivial. The second carries no algebraic structure at all beyond the zero of the target P, which is the one Function.Exact itself refers to: exactness sends every element of N into the range of f, and a trivial M makes that range trivial.

theorem TauCeti.finiteDimensional_of_exact {k : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [DivisionRing k] [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] [AddCommGroup P] [Module k P] {f : M →ₗ[k] N} {g : N →ₗ[k] P} (h : Function.Exact ⇑f ⇑g) [FiniteDimensional k M] [FiniteDimensional k P] : FiniteDimensional k N

If M --f--> N --g--> P is exact at N and both M and P are finite-dimensional, then so is N.

This is deduced from Module.Finite.of_exact, which asks the second map to be surjective, by corestricting g to its range.

theorem TauCeti.subsingleton_of_exact {M : Type u_1} {N : Type u_2} {P : Type u_3} [Zero P] {f : M → N} {g : N → P} (h : Function.Exact f g) [Subsingleton M] [Subsingleton P] : Subsingleton N

If M --f--> N --g--> P is exact at N and both M and P are trivial, then so is N.