nLab finite-dimensional vector space



Linear algebra

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts




A vector space is finite-dimensional if it admits a finite basis: if there exists a natural number nn such that the vector space admits a linear isomorphism to the direct sum of nn copies of the underlying vector space of the ground field.

The category FinDimVect of finite-dimensional vector spaces is of course the full subcategory of Vect whose objects are finite-dimensional.


Compact closure


A vector space VV is finite-dimensional precisely if the hom-functor hom(V,):VectSet\hom(V, -) \colon Vect \to Set preserves filtered colimits.


Notice that every vector space WW is the filtered colimit of the diagram of finite-dimensional subspaces WWW' \subseteq W and inclusions between them. Applying this to W=VW = V, the condition that hom(V,)\hom(V,-) preserves filtered colimits implies that the canonical comparison map from the following filtered colimit over the finite-dimensional subspaces is an isomorphism:

limfdVVhom(V,V)hom(V,V). \underset{ \underset {\mathclap{fd\, V' \subseteq V}} {\longrightarrow} }{\lim} \; \hom(V, V') \overset{\sim}{\longrightarrow} \hom(V, V) \mathrlap{\,.}

Therfore some element [f][f] in the colimit represented by f:VVf \colon V \to V' gets mapped to the identity id Vid_V, i.e., if=id Vi \circ f = id_V for some inclusion i:VVi \colon V' \hookrightarrow V. This implies ii is an isomorphism, so that VV is finite-dimensional.

In the converse direction, observe that hom(V,)\hom(V, -) has a right adjoint (and hence preserves all colimits) if VV is finite-dimensional.

To see this, first notice that the dual vector space V *V^\ast of functionals f:Vkf \colon V \to k to the ground field is a dual object to VV in the sense of monoidal category theory, so that there is a counit (evaluation map)

ev:V *V k fv f(v). \array{ \mathllap{ ev \,\colon\, } V^\ast \otimes V &\longrightarrow& k \\ f \otimes v &\mapsto& f(v) \mathrlap{\,.} }

The unit is uniquely determined from this counit and can be described using any linear basis e ie_i of VV and dual basis f jf_j as the map

coev:k VV * 1 ie if i. \array{ \mathllap{ coev \,\colon\, } k & \longrightarrow & V \otimes V^\ast \\ 1 &\mapsto& \sum_i e_i \otimes f_i \mathrlap{\,.} }

We thus have an adjunction

( kV)(V *), (- \otimes_k V) \;\;\dashv\;\; (- \otimes V^\ast) \,,

whose mate is, by the internal hom-adjunction ()Vhom(C,)(-) \otimes V \;\dashv\; hom(C,-) of this form:

hom(V,)hom(V *,) \hom(V, -) \;\dashv\; \hom(V^\ast, -)

exhibiting the desired right adjoint to hom(V,)hom(V,-).


Finite-dimensional vector spaces are exactly the compact objects of Vect in the sense of locally presentable categories, but also the compact = dualizable objects in the sense of monoidal category theory. In particular the category FinDimVect is a compact closed category.


Discussion of finite-dimensional vector spaces as categorical semantics for linear logic/linear type theory:

Last revised on September 12, 2023 at 06:21:10. See the history of this page for a list of all contributions to it.