Finitely generated modules

This file provides general results about Mathlib's category of finitely generated modules. Additivity of finite-free rank on biproducts makes dimension a split-additive invariant, which feeds the Grothendieck-group computation for finite-dimensional vector spaces.

Main results

• FGModuleCat.hom_hom_ofHom: the linear map underlying FGModuleCat.ofHom f is f, the analogue of Mathlib's ModuleCat.hom_ofHom.
• FGModuleCat.finrank_biprod: rank is additive on biproducts of finite free modules.

@[simp]

theorem FGModuleCat.hom_hom_ofHom {R : Type u} [Ring R] {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (f : V →ₗ[R] W) : ModuleCat.Hom.hom (ofHom f).hom = f

The linear map underlying FGModuleCat.ofHom f is f.

@[simp]

theorem FGModuleCat.finrank_biprod (R : Type u) [Ring R] [StrongRankCondition R] (X Y : FGModuleCat R) [Module.Free R ↑X] [Module.Free R ↑Y] : Module.finrank R ↑(X ⊞ Y) = Module.finrank R ↑X + Module.finrank R ↑Y

The rank of a biproduct of finite free modules is the sum of their ranks.