Grothendieck groups of finite-dimensional vector spaces

For a division ring k, FGModuleCat k is Mathlib's category of finite-dimensional left k-vector spaces. Every object is projective, so every short exact sequence in this category splits. Dimension is therefore additive for both split and abelian Grothendieck groups.

This file computes both groups. The dimension homomorphisms are upgraded to the additive equivalences TauCeti.SplitK0.finrankEquiv and TauCeti.AbelianK0.finrankEquiv. Every one-dimensional space has class a generator, and every object class is its dimension times that generator. The corresponding formulas for arbitrary additive invariants record the universal property in this concrete example. The equivalences assume Small.{v} k, ensuring that the carrier universe v contains a model of the one-dimensional space; this is automatic when the scalars and carriers live in the same universe.

Main results

• FGModuleCat.projective: every finite-dimensional vector space is projective.
• FGModuleCat.nonempty_splitting_of_shortExact: every short exact sequence of finite-dimensional vector spaces splits.
• TauCeti.SplitK0.finrankEquiv: split K₀ of finite-dimensional vector spaces is ℤ.
• TauCeti.AbelianK0.finrankEquiv: abelian K₀ of finite-dimensional vector spaces is ℤ.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Sections 5--6.

noncomputable def TauCeti.SplitK0.finrank (k : Type u) [DivisionRing k] : SplitK0 (FGModuleCat k) →+ ℤ

Dimension as a homomorphism from split K₀ of finite-dimensional vector spaces to ℤ.

Equations

• TauCeti.SplitK0.finrank k = TauCeti.SplitK0.lift (TauCeti.SplitK0.finrankInvariant✝ k)

@[simp]

theorem TauCeti.SplitK0.finrank_of (k : Type u) [DivisionRing k] (X : FGModuleCat k) : (finrank k) (of X) = ↑(Module.finrank k ↑X)

The dimension homomorphism sends an object class to its dimension.

theorem TauCeti.SplitK0.of_eq_finrank_nsmul (k : Type u) [DivisionRing k] (L X : FGModuleCat k) (hL : Module.finrank k ↑L = 1) : of X = Module.finrank k ↑X • of L

Every object class in split K₀ is its dimension times the class of the one-dimensional space.

noncomputable def TauCeti.SplitK0.finrankEquiv (k : Type u) [DivisionRing k] [Small.{v, u} k] : SplitK0 (FGModuleCat k) ≃+ ℤ

Dimension identifies split K₀ of finite-dimensional vector spaces with ℤ.

Equations

• TauCeti.SplitK0.finrankEquiv k = AddEquiv.ofBijective (TauCeti.SplitK0.finrank k) ⋯

@[simp]

theorem TauCeti.SplitK0.finrankEquiv_apply (k : Type u) [DivisionRing k] [Small.{v, u} k] (x : SplitK0 (FGModuleCat k)) : (finrankEquiv k) x = (finrank k) x

The dimension equivalence agrees with the dimension homomorphism.

theorem TauCeti.SplitK0.finrankEquiv_of (k : Type u) [DivisionRing k] [Small.{v, u} k] (X : FGModuleCat k) : (finrankEquiv k) (of X) = ↑(Module.finrank k ↑X)

The dimension equivalence sends an object class to its dimension.

theorem TauCeti.SplitK0.finrankEquiv_symm_apply (k : Type u) [DivisionRing k] [Small.{v, u} k] (L : FGModuleCat k) (hL : Module.finrank k ↑L = 1) (n : ℤ) : (finrankEquiv k).symm n = n • of L

The inverse dimension equivalence sends an integer to that multiple of the class of any one-dimensional space.

theorem TauCeti.SplitK0.AdditiveInvariant.obj_eq_finrank_nsmul (k : Type u) [DivisionRing k] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant (FGModuleCat k) G) (L X : FGModuleCat k) (hL : Module.finrank k ↑L = 1) : a.obj X = Module.finrank k ↑X • a.obj L

A split-additive invariant of finite-dimensional vector spaces is determined by its value on the one-dimensional space.

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

Dimension as a homomorphism from abelian K₀ of finite-dimensional vector spaces to ℤ.

Equations

• TauCeti.AbelianK0.finrank k = (TauCeti.SplitK0.finrank k).comp (TauCeti.AbelianK0.fromSplitEquiv✝ k).symm.toAddMonoidHom

@[simp]

theorem TauCeti.AbelianK0.finrank_of (k : Type u) [DivisionRing k] (X : FGModuleCat k) : (finrank k) (of X) = ↑(Module.finrank k ↑X)

The dimension homomorphism sends an object class to its dimension.

theorem TauCeti.AbelianK0.of_eq_finrank_nsmul (k : Type u) [DivisionRing k] (L X : FGModuleCat k) (hL : Module.finrank k ↑L = 1) : of X = Module.finrank k ↑X • of L

Every object class in abelian K₀ is its dimension times the class of the one-dimensional space.

noncomputable def TauCeti.AbelianK0.finrankEquiv (k : Type u) [DivisionRing k] [Small.{v, u} k] : AbelianK0 (FGModuleCat k) ≃+ ℤ

Dimension identifies abelian K₀ of finite-dimensional vector spaces with ℤ.

Equations

• TauCeti.AbelianK0.finrankEquiv k = (TauCeti.AbelianK0.fromSplitEquiv✝ k).symm.trans (TauCeti.SplitK0.finrankEquiv k)

@[simp]

theorem TauCeti.AbelianK0.finrankEquiv_apply (k : Type u) [DivisionRing k] [Small.{v, u} k] (x : AbelianK0 (FGModuleCat k)) : (finrankEquiv k) x = (finrank k) x

The dimension equivalence agrees with the dimension homomorphism.

theorem TauCeti.AbelianK0.finrankEquiv_of (k : Type u) [DivisionRing k] [Small.{v, u} k] (X : FGModuleCat k) : (finrankEquiv k) (of X) = ↑(Module.finrank k ↑X)

The dimension equivalence sends an object class to its dimension.

theorem TauCeti.AbelianK0.finrankEquiv_symm_apply (k : Type u) [DivisionRing k] [Small.{v, u} k] (L : FGModuleCat k) (hL : Module.finrank k ↑L = 1) (n : ℤ) : (finrankEquiv k).symm n = n • of L

The inverse dimension equivalence sends an integer to that multiple of the class of any one-dimensional space.

theorem TauCeti.AbelianK0.AdditiveInvariant.obj_eq_finrank_nsmul (k : Type u) [DivisionRing k] {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant (FGModuleCat k) G) (L X : FGModuleCat k) (hL : Module.finrank k ↑L = 1) : a.obj X = Module.finrank k ↑X • a.obj L

A short-exact-additive invariant of finite-dimensional vector spaces is determined by its value on the one-dimensional space.