@DanielSank The prof who promised to hire me last semester has decided he doesn't have enough money for me...I was supposed to start on a Raman project soon :/
Define the trace in an abstract way, define a vector space to be finite-dimensional of dimension $n$ when the trace of the identity is $n$. Problem solved.
@0celo7 The trace is the linear map $\mathrm{tr} : V^\ast\otimes V\to\mathbb{R}$ induced by the bilinear map $V^\ast\times V\to\mathbb{R}, (f,v) = f(v)$.
Okay. Now what hinders you to write $\mathrm{tr}(\mathrm{id}) = n$?
Or, rather, you can make $\delta$ define an element in $V\otimes V^\ast$, but that is not what we are doing. We are using the universal property to get the trace map $V^\ast \otimes V\to\mathbb{R}$ from the bilinear map $\delta$ (if you are troubled by the word "induced", just don't use it :P)
@ACuriousMind It should then be clear that I in no way have any idea how to prove this implies the existence of $n$ linearly independent vectors that span $V$.
@ACuriousMind I think the other way around is easier, one can construct $\delta^i{}_j$ and sum diagonal elements.
@0celo7 Then just choose a modification of the definition of dimension that you're more comfortable with. You could e.g. define the dimension of a vector space $V$ by the maximal length of a chain of true inclusions $\{0\}\subset V_1\subset V_2\subset V_3\subset\dots V$.
That also makes no reference to a basis and thus also resolves the circular reasoning problem
@yuggib I thought the issue is that we want the statement "finite-dimensional vector spaces have a basis" to not be circular because we defined "finite-dimensional" by having a finite basis.
Of course, no matter how you define dimensions, the statement "infinite-dimensional vector spaces have a basis" will fail without choice
Well, you can take my definition for the dimension and add "if no finite chain of maximal length exists, the space is infinite-dimensional". What's the problem with that?
If universal wavefunction interpretation is to be believed, wouldn't it account for matter/antimatter asymmetry?
I mean, the chance in the early universe to have significantly more matter than antimatter is small, too small, but if it is not zero, we simply happened to live in the improbably small part of the universe's wavefunction that there exists enought baryonic matter for life to be possible, right?
Ok, $tr:V\otimes V^*\to\mathbb{R}$ is the unique bilinear map induced by the natural pairing $V\times V^*\to\mathbb{R},(f,v)\mapsto f(v)$. Uniqueness follows from the universal property of $\otimes$.
@0celo7 Then just choose a modification of the definition of dimension that you're more comfortable with. You could e.g. define the dimension of a vector space $V$ by the maximal length of a chain of true inclusions $\{0\}\subset V_1\subset V_2\subset V_3\subset\dots V$.
