Finrank of a zero object of ModuleCat #
Vanishing of an object of ModuleCat R is naturally expressed categorically, as
CategoryTheory.Limits.IsZero, while the dimension counts that consume it speak of
Module.finrank. This file supplies the one translation between the two: a zero object has
finrank zero.
That translation is what bounds the Module.finrank support of a bounded complex of vector
spaces by its bounding interval, which is in turn what makes Mathlib's finsum-based Euler
characteristic of such a complex an honest finite sum.
theorem
ModuleCat.finrank_eq_zero_of_isZero
{R : Type u}
[Ring R]
[Nontrivial R]
{X : ModuleCat R}
(hX : CategoryTheory.Limits.IsZero X)
:
A zero object in ModuleCat R has finrank zero.