Return to Answer

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.

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.

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.

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.

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.

Vice versa, a trace operator does not exist if $V$ is infinite dimensional -- because then $T(I)$ does not exist for the identity map $I$.

So, we have a basis-free

Definition 2: A linear space $V$ is finite dimensional if a trace operator (as defined in Definition 1) exists (which will then be 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 exists 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 exists for finite-dimensional spaces is completely trivial, in fact tautological -- and it does not seem to pick a basis in any apparently reasonable sense.

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.

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.

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.

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.

Vice versa, a trace operator does not exist if $V$ is infinite dimensional. Indeed, if $(e_j)_{j\in J}$ is a basis of $V$, where $J\supseteq\Bbb N$, let $A\in L(V)$ be defined by the condition that $A(e_j)=1(j\in\Bbb N)$ for all $j\in J$. Then $T(A)$ does not exist in $F$.

So, we have a basis-free

Definition 2: A linear space $V$ is finite dimensional if a trace operator (as defined in Definition 1) exists (which will then be 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 exists 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 exists for finite-dimensional spaces is completely trivial, in fact tautological -- and it does not seem to pick a basis in any apparently reasonable sense.

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.

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.

Vice versa, a trace operator does not exist if $V$ is infinite dimensional -- because then $T(I)$ does not exist for the identity map $I$.

So, we have a basis-free

Definition 2: A linear space $V$ is finite dimensional if a trace operator (as defined in Definition 1) exists (which will then be 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 exists 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 exists for finite-dimensional spaces is completely trivial, in fact tautological -- and it does not seem to pick a basis in any apparently reasonable sense.