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:
The trace of an endomorphism, defined by choosing a basis.
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 these choices. So they should still exist in a 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 things like in 1. 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 things like in 1. exist. Where exactly does the above informal "philosophical" argument fail? What is the deeper reason for the existence (or nonexistence) of such objects?