Rank--nullity at an exact middle term

LinearMap.finrank_range_add_finrank_ker splits the dimension of the source of a linear map into rank and nullity. At the middle term of an exact pair A → B → C the kernel of the second map is the range of the first, so the dimension of B is the sum of the two ranks around it. Both alternating-sum arguments, the bounded one in Algebra/Exact/Sequence.lean and the ℤ-indexed one in Algebra/Homology/EulerCharacteristic.lean, consume this.

k is a division ring, not a field: that is what LinearMap.finrank_range_add_finrank_ker asks for, and commutativity is used nowhere.

theorem Function.Exact.finrank_eq_finrank_range_add_finrank_range {k : Type u_1} [DivisionRing k] {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module k A] [Module k B] [Module k C] [Module.Finite k B] {f : A →ₗ[k] B} {g : B →ₗ[k] C} (h : Exact ⇑f ⇑g) : Module.finrank k B = Module.finrank k ↥f.range + Module.finrank k ↥g.range

Rank--nullity at an exact middle term: an exact A → B → C splits dim B into the two ranks around it.

theorem Function.Exact.module_finite_of_finite {k : Type u_1} [DivisionRing k] {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module k A] [Module k B] [Module k C] {f : A →ₗ[k] B} {g : B →ₗ[k] C} (h : Exact ⇑f ⇑g) [Module.Finite k A] [Module.Finite k C] : Module.Finite k B

The middle term of an exact pair between finite modules is finite.

B is generated by a generating set of the kernel of g, which is the range of f and so finite, together with lifts of a generating set of the range of g, a submodule of the finite C. This is the step a dévissage takes at every degree: Hⁱ(G) → Hⁱ(F) → Hⁱ⁺¹(K) with the outer terms finite-dimensional.