Precise meaning of "picking a basis"?

This will not answer Timothy Chow's question about formalizing a sense of "needing to pick a basis as part of the proof", but rather it is a probing of the apparent skepticism that a basis-free proof is possible.

As I remarked in comments under the original post, if we work over arbitrary commutative rings $R$, one can define a trace operation

$$\hom_R(P, P) \to R$$

so long as $P$ is finitely generated projective over $R$. The idea is to establish that the canonical transformation

$$\phi_Q: P^\ast \otimes_R Q \to \hom_R(P, Q) \qquad f \otimes q \mapsto (p \mapsto f(p)q),$$

natural in $R$-modules $Q$, is an isomorphism. Then the trace is the composite

$$\hom_R(P, P) \overset{(\phi_P)^{-1}}{\to} P^\ast \otimes_R P \overset{\mathrm{ev}}{\to} R$$

where $\mathrm{ev}$ denotes the evaluation map $f \otimes p \mapsto f(p)$.

This is a perfectly "basis-free" description. Of course, in proving the claim that $\phi_Q$ is an isomorphism, one has to use the fact that $P$ is finitely generated projective somewhere; one could hardly do otherwise! And that fact is none other than the fact that $P$ is the image of some idempotent map $e: R^n \to R^n$.

Proof of claim: by naturality, there is a commutative diagram

$$\begin{array}{ccccc} (R^n)^\ast \otimes_R Q & \twoheadrightarrow & P^\ast \otimes_R Q & \rightarrowtail & (R^n)^\ast \otimes_R Q \\ \downarrow \cong & & \downarrow \phi_Q & & \downarrow \cong \\ \hom_R(R^n, Q) & \twoheadrightarrow & \hom_R(P, Q) & \rightarrowtail & \hom_R(R^n, Q) \end{array}$$ where both rows are image factorizations of idempotent maps induced by $e$, and the vertical maps on the boundaries are clearly isomorphisms (by canonically identifying their domains and codomains with $Q^n$). Now $\phi_Q$ is epic because its composition with the top left arrow is epic, and $\phi_P$ is monic because its composition with the bottom right arrow is monic. Being monic and epic, $\phi_Q$ is an isomorphism. $\Box$

It can't be literally correct that we "picked a basis" (of $P$) in order to describe the trace on $\hom_R(P, P)$. The most we did is exploit one of the definitions of f.g. projective module, involving images of idempotent matrices $e$, in order to validate the claim that the natural map $\phi_P$ is invertible (what we did is show that its relational opposite $(\phi_P)^{-1}$ is a well-defined function).

So if you like, you can view trace as defined above initially as a relational composite $\mathrm{ev} \circ (\phi_P)^{op}$, and then verify as we did that the relation you get this way is in fact a well-defined function.

Just a few more remarks: the first comment I made under the original post was [in retrospect!] a kind of response to Timothy's comment to Andrej Bauer: "Right, that's why I was hoping for something along the lines of, setting up axioms that capture most of linear algebra, but where "finite-dimensional" vector spaces don't necessarily have a basis." The idea I had is that we generalize from ordinary linear algebra over a field $k$ to linear algebra over slightly more general sorts of rings $R$, where we might not have the luxury that finitely generated $R$-modules have bases, thus forcing us to do things differently.

So, if for example $R$ (again commutative) is a Noetherian von Neumann regular ring, then those are sufficient to guarantee that any finitely generated module is in fact finitely generated projective, and then set up trace as above. I think readers will be able to figure this out mostly on their own, perhaps with a few hints: (1) the Noetherian assumption is used to ensure that finitely generated modules are finitely presentable, and (2) finitely presentable modules over a von Neumann regular ring are projective; this uses some of the lore of von Neumann regular rings, which you can find in the nLab article on vN regular rings, particularly lemmas 2.3 and 2.4 (see there). Of course, commutative vN regular rings are not exactly a huge departure from the comfort of fields!

Here is a construction which never "picks a basis". It refers to the fact that a finite basis exists by definition of "finitely-dimensional vector space" (so hardly avoidable), and it does so only in the proof of a logical statement, i.e., not a construction.

First allow me to clarify a point about formal logic: not every informal use of “pick” indicates choice. In particular, when an assumption $\exists x \in X . \phi$ is available and we proceed to prove a logical statement $\psi$ by saying "pick $x \in X$ such that $\phi$" – that's not the axiom of choice but just an elimination of existential quantifier, which is a logical inference rule.

Given a vector space $V$ over $\mathbb{R}$, let $$ T_V = \{ t \in \mathsf{Lin}(\mathsf{End}(V), \mathbb{R}) \mid \forall A, B \in \mathsf{End}(V) .\, t(A \circ B) = t(B \circ A)\}. $$ In words, $T_V$ is the linear subspace of cyclic linear functionals on endomorphisms of $V$.

Given a linear isomorphism $\alpha : V \to W$, define the maps $b_\alpha : T_V \to T_W$ and $c_\alpha : T_W \to T_V$ by $$ b_\alpha(t)(B) = t(\alpha^{-1} \circ B \circ \alpha) \qquad\text{and}\qquad c_\alpha(u)(A) = u(\alpha \circ A \circ \alpha^{-1}). $$ It is easy to check that $b_\alpha$ and $c_\alpha$ form a linear isomorphism between $T_V$ and $T_W$. Moreover, we have $b_\alpha(t)(\mathsf{id}_W) = t(\mathsf{id}_V)$ for all $t \in T_V$, and similarly for $c_\alpha$.

For any $k \in \mathbb{N}$, define $S^k_V = \{t \in T_V \mid t(\mathsf{id}_V) = k\}$. If $\alpha : V \to W$ is a linear isomorphism, then $c_\alpha$ restricts to a bijection $S^k_W \to S^k_V$.

Now suppose there exists $n \in \mathbb{N}$ and a linear isomorphism $\alpha : V \to \mathbb{R}^n$, i.e., $V$ is finite-dimensional. It is known from the standard construction of trace on $\mathbb{R}^n$ that $S^n_{\mathbb{R}^n}$ is a singleton which contains precisely the standard trace operator on $\mathbb{R}^n$. Consequently, $S^n_V$ is a singleton too, so we may define the trace operator on $V$ as the unique element of $S^n_V$.

Have I "picked an isomorphism $\alpha : V \to \mathbb{R}^n$"? I certainly mentioned it, but that was imposed on me by the definition of “finite-dimensional”. I made no choice of $\alpha$, and neither did I have to show that any construction I made was invariant in $\alpha$. I only used $\exists$-elimination to prove $$ (\exists \alpha : V \to \mathbb{R}^n .\, \text{$\alpha$ is a linear isomorphism}) \implies \exists t \in S^n_V . \forall u \in S^n_V .\, t = u. $$ If I am not allowed to use first-order logic, then I give up.

One last remark: at the very end we used the following fact: if a set $M$ contains precisely one element, then we may extract the element from $M$. We can indeed, in set theory the element is simply $\bigcup M$.

P.S. As far as I can tell, the whole argument is constructively valid.

In quantum physics we sometimes refer to a definition from category theory: Since there is no functorial choice of basis, a proof picks a basis if it defines a non-functorial construction.

In quantum mechanics “picking a basis” is equivalent to assigning sharp values simultaneously to a complete set of observables. For example, this could be the three coordinates $x,y,z$, or it could be the three momentum components $p_x,p_y,p_z$. The obstruction to a functorial choice of basis is expressed by the Kochen-Specker theorem: It is not possible to assign values to all observables. This implies that you cannot avoid picking a basis if you want to describe a measurement.

This does not answer the highlighted question by the OP, on whether it is possible in general to formalize what it means for a proof to pick a basis. However, we can comment on this as far as the notion of the trace is concerned. Perhaps most importantly, a basis-free definition of a finite-dimensional linear space is provided.

Specifically, let us first give a basis-free definition of the trace: Let $V$ be a vector space over a field $F$, and let $L(V)$ be the vector space over $F$ of all linear maps from $V$ to $V$. For each linear functional $\ell\colon V\to F$ and each $v\in V$, define the linear map $A_{\ell,v}\in L(V)$ by the formula $$ A_{\ell,v}(x):=\ell(x)v$$ for all $x\in V$.

Definition 1: A trace operator is a linear map $T\colon L(V)\to F$ such that $$T(A_{\ell,v})=\ell(v)$$ for all $v\in V$ and all linear functionals $\ell\colon V\to F$.

Remark: As noted in Will Sawin's comment, this definition is essentially equivalent to the one given in Kevin Buzzard's blog post, who noted that it is already in Wikipedia. However, the Wikipedia definition is in terms of the tensor product and its universal property, and the Wikipedia definition is much longer and less elementary.

A trace operator (as defined in Definition 1) exists and is unique for finite-dimensional spaces $V$. Indeed, let $E=(e_1,\dots,e_n)$ be a basis of $V$ and let $(\ell_1,\dots,\ell_n)$ be the dual basis of the space $V'$ of all linear functionals on $V$. Then for all $x\in V$ and all $i\in[n]$ $$A_{\ell_i,e_i}(x)=x_i e_i,$$ the $i$th vector component of $x$ wrt to the basis $E$, where $x_i$ is the $i$th coordinate of $x$ wrt to $E$. One can express any $A\in L(V)$ as a linear combination of the $A_{\ell_i,e_i}$'s, and then go from there.

More generally, as noted in the comment by Emil Jeřábek, the values of $T(A)$ are uniquely determined by Definition 1 for $A\in L_0(V)$, where $L_0(V)$ is the space of all maps in $L(V)$ with a finite-dimensional range. One can then extend $T$ from $L_0(V)$ to $L(V)$ by defining $T$ arbitrarily but linearly on a direct complement $L_1(V)$ of $L_0(V)$ to $L(V)$.

So, we have a basis-free

Definition 2: A linear space $V$ is finite dimensional if a trace operator (as defined in Definition 1) is unique.

Now, on the question by the OP, on whether it is possible to formalize what it means for a proof to pick a basis. As far as the notion of the trace is concerned, one may ask: a proof of what?

A proof that a basis-free definition is equivalent to the usual, matrix definition of the trace? But the matrix definition is given in terms of a basis (even if the value of the trace does not depend on the choice of the basis) -- so, such a proof is impossible.

A proof that a trace operator is unique for finite-dimensional spaces $V$? Then the problem is to define finite-dimensional in a basis-free way. That was done above in Definition 2, and then the proof that a trace operator is unique for finite-dimensional spaces is completely trivial, in fact tautological -- and it does not seem to pick a basis in any apparently reasonable sense.

I am not sure this answers the question, but I still wanted to provide another (geometric) viewpoint.

My issue with the other answers talking about $\text{Hom}(V,V) \cong V^* \otimes V$ is that in order to actually calculate the trace of a linear $T:V\to V$, I have to first write it in the form of something in $V^* \otimes V$. So thinking in terms of the computational process, I do have to choose a basis.

But using the geometric interpretation of trace, I don't have to do this. Suppose I have a blank piece of paper, with a single black dot on it, called $0$. Purely geometrically, I can work with the vector space structure (e.g. parallelogram rule for addition, etc.) If you further allow me to draw one ball $\frak B$ centered at $0$, and have access to the Haar measure on $V$ (the unique such assigning volume 1 to the ball I drew --- this doesn't require picking a basis) then I can calculate the trace as follows:

$$\text{tr}(T) := \lim_{t\to 0} \frac{\mu((I+tT)\frak B) - \mu(\frak B)}{t}$$

Never once did I have to prioritize a certain direction on my piece of paper; I just needed 1 dot ($0$) and 1 ball. But why is choosing a distinguished shape (ball) better than a distinguished basis?

I think the answer lies in Samra's comment about vector bundles. Consider the Mobius band as a line bundle over the circle $S^1$. Then there is no continuous choice of basis! But there is a continuous choice of ball (i.e. continuous choice of norm, which gives rise to a unit ball).

Allow me a digression to another field.

In the field of Borel combinatorics, one way of [thinking about]/[limiting] the amount of choices one makes is by having (continuum) many copies of the same object, and trying to do a process on all of them without using the axiom of choice.

For example, consider the graph with vertex set $V = \{z\in \mathbb C: |z|=1\}$ and edge set $E = \{ \{z, e^{i\alpha}z\}: z\in V\}$ and $\alpha$ an irrational multiple of $\pi$. Every connected component of this graph is a copy of (the Cayley graph w.r.t. generators $\pm 1$ of) $\mathbb Z$, so the chromatic number is 2. But (using for instance measure theory) one can show that there is no Borel (nor Lebesgue-measurable) 2-coloring $c: V\to 2$. This formalizes in some sense that in order to get a 2-coloring one must "pick a starting vertex" in each connected component (of which there are continuum many).

So this tells us that "picking a distinguished vertex in a copy of $\mathbb Z$" is not very "natural", because there is an example of a "natural" setting with infinitely many copies of $\mathbb Z$ in which there is no Borel way of picking a distinguished vertex in each copy.

Likewise, "picking a basis in a copy of $\mathbb R$" (each fiber in the Mobius bundle) is not very "natural", because there is an example of a "natural" setting with infinitely many copies of $\mathbb R$ in which there is no continuous way of picking a distinguished basis vector in each copy. However, there is a continuous way of picking a distinguished ball in each copy.

Hopefully this communicates some sense in which "picking a basis" is not natural, and how one can avoid this "non-naturality" but still compute the trace.

(Maybe in fact one can define a version of the trace for all $\sigma$-compact locally compact abelian groups --- which admit Haar measure, and an equivariant distance function leading to a compact unit ball, I think)

I personally feel the question is not well defined, and unclear what would constitute an answer — the following is a general strategy in constructive math to turn constructive a construction which involves the axiom of choice but where the result of the construction actually doesn't depend on the choice made using the axiom of choice, which it seems to me can be used here — though it is a little strange as existence of a finite basis ends up being literally the definition of finite dimensionsal space, despite this at no point in the following argument can one say I'm picking a basis. Technically the result that corresponds to the existence of a basis is the first lemma below — but that lemma is provable constructively even for infinite dimensional space, so it wouldn't be correct to say it proves the existence of a basis.

$\DeclareMathOperator\span{span}$Let $V$ be a vector space over a field $k$. We can consider the geometric theory of bases of $V$. It is the propositional theory of subsets $S \subseteq V$ which satisfy the following axioms: first for each $v \in V$ an axiom that says

$$ \bigcup \left( (v_1 \in S) \land \dots \land (v_n \in S) \right)$$ where the union is over all tuples of $v_1,\dots,v_n \in V$ such that $v \in \span(v_1,\dots,v_n)$.

and the collection of axioms

$$ v_1 \in S \land \dots \land v_n \in S \implies (\lambda_1=\dots=\lambda_n=0) \cup \bigcup_{i \neq j} (v_i = v_j ) $$ for each $n$-uples of elements $(v_1, \dotsc, v_n)$ and scalars $(\lambda_1, \dotsc, \lambda_n)$ such that $\lambda_1 v_1 + \dots + \lambda_n v_n =0$.

We can hence construct the classifying locale $B(V)$ of bases of $V$ — a point of $B(V)$ would be a basis of $V$, but we won't need to know that a point exists.

I claim that:

Lemma: Constructively, assuming $V$ and $k$ have decidable equality, then one can show that the map $B(V) \to 1$ is an open surjection.

proof I haven't checked all the details to be honest, but the idea is that the basic opens of $B(V)$ are the "$v_1 \in S \land \dots \land v_n \in S$" we can define it to be positive if the $v_i$ are a free family and this should give us a positivity predicate for $B(V)$.

We can then define:

Definition: a vector space is of dimension $n$ for some integer if the universal basis has size $n$.

By "the universal basis" I mean the subsheaf of the constant sheaf equal to $V$ over $B(V)$ corresponding to the "$S$" of the theory. Note that under the assumption that $V$ is decidable, the universal basis is a decidable sheaf over $B(V)$, so its size can be define as a semi-continuous function $B(V) \to \mathbb{N} \cup \{\infty\} $ so it makes sense to ask it to just be $n$. When it is the case, the universal basis is actually (Kuratowski) finite.

Finally, given any operator $f:V \to V$, we can define its trace as a functions on $B(V) \to k$ which we can show is constant in the sense that $B(V) \times B(V) \to k \times k$ factors through $k \subseteq k \times k$. This will be the usual proof that the trace is independent of the basis applied internally to $B(V) \times B(V)$.

As we know $B(V) \to 1$ is an open surjection constant functions $B(V) \to k$ correspond to elements of $k$.

At no point in this argument do we need to use that the locale $B(V)$ actually has a point, we are only using that $B(V) \to 1$ is an open surjection, which can be proved without choice even for infinite dimensional vector spaces — though it can be shown that under the assumption that $V$ is finite dimensional the locale $B(V)$ is actually discrete.