Finrank as an additive invariant

This file packages finrank on finite-dimensional vector spaces as an invariant additive on short exact sequences. It is the reusable bridge from FGModuleCat to abelian Grothendieck groups.

Additivity has to be read off from ModuleCat.free_shortExact_finrank_add, which lives one category down, so the file first records how the forgetful functor forget₂ (FGModuleCat k) (ModuleCat k) interacts with finrank. This is the only place where the definitional identification of an FGModuleCat object with its underlying module is used; everything else goes through it.

@[simp]

theorem FGModuleCat.finrank_forget₂_obj {R : Type u} [Ring R] (X : FGModuleCat R) : Module.finrank R ↑((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).obj X) = Module.finrank R ↑X

Forgetting the finite-generation witness does not change finrank.

noncomputable def TauCeti.AbelianK0.AdditiveInvariant.finrank (k : Type u) [DivisionRing k] : AdditiveInvariant (FGModuleCat k) ℤ

Finrank on FGModuleCat k, as a ℤ-valued invariant additive on short exact sequences.

The definition is sealed; use finrank_obj to evaluate it on an object.

Equations

• TauCeti.AbelianK0.AdditiveInvariant.finrank k = { obj := fun (X : FGModuleCat k) => ↑(Module.finrank k ↑X), map_shortExact := ⋯ }

@[simp]

theorem TauCeti.AbelianK0.AdditiveInvariant.finrank_obj (k : Type u) [DivisionRing k] (X : FGModuleCat k) : (finrank k).obj X = ↑(Module.finrank k ↑X)

Evaluate the finrank additive invariant as the integer-valued module finrank.