Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Chosen bases exhibit as equivalent to finite-dimensional vector spaces
Example
Let have natural numbers as objects and matrices as morphisms . The coordinate functor identifies it, up to equivalence, with the category of finite-dimensional -vector spaces.
Facts & Assumptions
Given: A field and, for every finite-dimensional -vector space, a supplied ordered basis.
Finite-dimensional vector spaces form a full subcategory of (Subcategory and full subcategory, Vector spaces over a fixed field and linear maps form the large locally small category ).
Matrix multiplication is associative and has identity matrices, including the zero-dimensional cases (Rectangular matrix multiplication and the identity matrix , including zero-sized shapes, Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication).
Linear maps in chosen coordinates correspond bijectively to matrices, and composition corresponds to matrix multiplication (Coordinate columns and matrices of linear maps relative to ordered bases, is a vector-space isomorphism , ).
Equal dimension characterizes isomorphism of finite-dimensional spaces (Two finite-dimensional vector spaces over are linearly isomorphic if and only if they have the same dimension).
A fully faithful, split essentially surjective functor is an equivalence (Covariant functor, identity functor, composite functor, and contravariant functor, Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors, Equivalence, quasi-inverse, and adjoint equivalence of categories, A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice).
Verification
By [L2], matrix multiplication and identity matrices make a category. Define by and by letting be multiplication by the matrix .
Identity and composition are preserved by [L2] and [L3], so is a functor.
For every , the map is the coordinate bijection from matrices to linear maps . Thus is fully faithful.
Suppose an ordered basis has been supplied for each finite-dimensional vector space . If its length is , the coordinate map is a specified isomorphism, including when . Hence these choices split essential surjectivity.
The criterion in [L5] now makes an equivalence. Thus chosen bases turn arbitrary finite-dimensional spaces into coordinate models without asserting that the two categories are strictly identical.
Depends on
- Subcategory and full subcategory
- Covariant functor, identity functor, composite functor, and contravariant functor
- Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors
- Equivalence, quasi-inverse, and adjoint equivalence of categories
- A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice
- Vector spaces over a fixed field and linear maps form the large locally small category $\mathbf{Vect}_F$
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
- Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication
- Coordinate columns $[v]_{\mathcal B}$ and matrices $[T]_{\mathcal B}^{\mathcal C}$ of linear maps relative to ordered bases
- $T\mapsto[T]_{\mathcal B}^{\mathcal C}$ is a vector-space isomorphism $\mathcal L(V,W)\cong M_{m\times n}(F)$
- $[S\circ T]_{\mathcal B}^{\mathcal D}=[S]_{\mathcal C}^{\mathcal D}[T]_{\mathcal B}^{\mathcal C}$
- Two finite-dimensional vector spaces over $F$ are linearly isomorphic if and only if they have the same dimension
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Emily Riehl, Category Theory in Context, Example 1.5.12 (standard reference, not scraped)