It happens a lot of times that when one defines a new object (ring, module, space, group, algebra, morphism, whatever) out of given data one first chooses some additional structure. And sometimes (often?) the constructed object a posteriori happens to be independent of the choice.
Examples which come to mind are the following:
1. The trace of an endomorphism, defined by choosing a basis
2. Derived functors like $Ext$, $Tor$, defined by choosing projective/injective resolutions
Now I have the feeling, that "natural" objects that are not dependent on choices should exist independently of that choices. So they should still exist in an universe where there's no way to choose and so I would expect that existence to be provable there. So I would expect there to be some way to avoid choosing anything in the first place in order to define such objects.
For instance, one can define the trace as the composite map: $End_k(V)\cong V^*\otimes V \to k$ where $V^ *\otimes V\to k$ is evaluation and $V^ *\otimes V \to End_k(V)$ is given by $f\otimes v\mapsto (w\mapsto f(w)v)$.
So my questions are the following:
- Do you know examples of things which are natural in some sense but which can't be defined without choosing something first?
- Are $Ext$, $Tor$, etc. examples? i.e. is there a way to define derived functors without choosing resolutions?
- If such things to exist, is there some way to make the statement precise that they can't be defined without choosing anything? Can such results be proven?
- Assuming again something like this exists. Where exactly does the above informal "philosophical" argument fail? What is the deeper reason for the existence (or nonexistence) of such objects?