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
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
A vector space is finite-dimensional if it admits a finite basis: if there exists a natural number $n$ such that the vector space admits a linear isomorphism to the direct sum of $n$ 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.
A vector space $V$ is finite-dimensional precisely if the hom-functor $\hom(V, -) \colon Vect \to Set$ preserves filtered colimits.
Notice that every vector space $W$ is the filtered colimit of the diagram of finite-dimensional subspaces $W' \subseteq W$ and inclusions between them. Applying this to $W = V$, the condition that $\hom(V,-)$ preserves filtered colimits implies that the canonical comparison map from the following filtered colimit over the finite-dimensional subspaces is an isomorphism:
Therfore some element $[f]$ in the colimit represented by $f \colon V \to V'$ gets mapped to the identity $id_V$, i.e., $i \circ f = id_V$ for some inclusion $i \colon V' \hookrightarrow V$. This implies $i$ is an isomorphism, so that $V$ is finite-dimensional.
In the converse direction, observe that $\hom(V, -)$ has a right adjoint (and hence preserves all colimits) if $V$ is finite-dimensional.
To see this, first notice that the dual vector space $V^\ast$ of functionals $f \colon V \to k$ to the ground field is a dual object to $V$ in the sense of monoidal category theory, so that there is a counit (evaluation map)
The unit is uniquely determined from this counit and can be described using any linear basis $e_i$ of $V$ and dual basis $f_j$ as the map
We thus have an adjunction
whose mate is, by the internal hom-adjunction $(-) \otimes V \;\dashv\; hom(C,-)$ of this form:
exhibiting the desired right adjoint to $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:
Benoît Valiron, Steve Zdancewic, Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi, in: Proc. of ICTAC’14, Lecture Notes in Computer Science 8687, Springer (2014) 442-459 [arXiv:1406.1310, doi:10.1007/978-3-319-10882-7_26, slides:pdf, pdf]
(focus on finite ground fields)
Daniel Murfet, Logic and linear algebra: an introduction [arXiv:1407.2650]
Last revised on September 12, 2023 at 06:21:10. See the history of this page for a list of all contributions to it.