Objects which can't be defined without making choices but which end up independent of the choice 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?

 A: A possible example of what you're looking for, though of a somewhat different character from the examples given so far, is [the] "algebraic closure of $\mathbb Q$."  Läuchli (Auswahlaxiom in der Algebra, Comment. Math. Helv. 37 (1962), 1–18) showed that ZF does not prove the uniqueness of the algebraic closure of $\mathbb Q$.  However, it is very easy to construct an algebraic closure of $\mathbb Q$ in ZF.  So in some sense there is provably no way to define "the" algebraic closure of $\mathbb Q$ unless we give ourselves the power of making arbitrary choices, via the axiom of choice.  This example is a little peculiar, though, since what the ability to make arbitrary choices is needed for is not to construct an instance of the object, but rather to prove the equivalence of different constructions.
Of a similar flavor is the construction of "the" hyperreals as an ultrapower, which is unique up to isomorphism if you assume the continuum hypothesis.
A: The Seiberg-Witten invariant of an oriented  compact manifold $4$-manifold needs at least a metric and often an additional $2$-form  to be defined. Ultimately it is independent of the choice of metric and form
A: To my knowledge, the "pushforward with compact supports" along $f \colon X \to Y$ for étale cohomology is such a thing.  For topological spaces it is easy to define
$$f_!\mathcal{F}(U) = \{ s \in \mathcal{F}(f^{-1}U) \mid f|_{\operatorname{supp}(s)} \text{ is proper}\}$$
(you know, as the name says) but this relies on $U$ actually being a subset of $Y$, so for étale sheaves one simply chooses a factorization of $f$ as a composition $p \circ j$, where $p$ is proper and $j$ is an open immersion; for $p$, we define $p_! = p_*$, while for $j$ we take $j_!$ to be "extension by zero" which does work even in the étale topology; then $f_! = p_! j_!$.
There are many such factorizations (that is, many compactifications of $f$); that one even exists in general, under some finiteness hypotheses, is a theorem of Nagata, but as for vector space bases, there is no canonical one.  And unlike for bases, there is also no "maximal object" in the class of functors obtained from these choices; they are all simply canonically isomorphic to each other.
A: Well-ordering of the real numbers, or just any arbitrary set. Although this is somewhat inaccurate. So we can require a slightly more explicit requirement, well-ordering of a minimal order type.
The minimal order type, if any exists, is unique. But in order to have one to begin with, we need to make plenty of choices.
One more for the road, which is not entirely up to the requirements here, but deserves a mention after all, is a Vitali set. We have to make quite a few of choices in order to prove that one exists. And although in a good sense many are non-isomorphic (they can have outer measure as large and as small as we want it to be), the one property we are interested in is independent of that choice -- all Vitali sets are non-measurable.
A: I doubt that you can define addition and multiplication on the real numbers (defined as equivalence classes of Cauchy sequences) without making choices.  
[Edited to add:  As Toink points out in comments, it's actually quite easy to define addition and multiplication without making choices. So let me modify the above by replacing "addition and multiplication on the real numbers" with "the square root function on the positive real numbers".]
In general, when an infinite set (or, say, an infinitely generated group, etc) is defined via an equivalence relation, as often happens in mathematics, there's no avoiding the fact that functions on that set have to be defined by choosing representatives (unless, of course, you first prove that your definition is equivalent to some other definition --- e.g. the reals can also be defined by Dedekind cuts --- but that only pushes the making of choices back a step, into the proof that the definitions are equivalent).
(One class of exceptions:  If you're defining a function into an ordered set, you can avoid making choices by defining the value of your function to be its maximum over all possible choices --- this works for, say, the dimension of a vector space.  But if the function's codomain has no extra structure, it seems clear that choices are unavoidable. Edited to add: Again, per Toink's comment, another class of exceptions occurs when the structure on the quotient is inherited from above.)
A: I don't know of a way to completely formalize your question, but here is something with the same flavor that may hint at how to proceed.  Blass and Gurevich defined a complexity class—or more accurately, a logic—that they called "Choiceless Polynomial Time with Counting" or $\tilde CPT+Card$.  The exact definition is somewhat technical (their paper is easily findable with Google) but roughly speaking, the idea is that the properties of unlabeled graphs that are expressible in $\tilde CPT + Card$ are precisely those that are computable in polynomial time without choosing a labeling of the graph.  I believe that it is still an open question whether every polynomial-time computable property of unlabeled graphs, including those that proceed by labeling the graph and then computing some property that ends up being independent of the labeling, is expressible in $\tilde CPT+Card$.  I think most people expect the answer to be no, but it's not easy to come up with a candidate to separate the two classes.  This question is closely related to the question of whether graph isomorphism is solvable in polynomial time.
Of course, what you're interested in doesn't involve any computational limitations.  However, the above discussion suggests that if you wanted to formally prove that some particular property of an object requires an arbitrary choice, then you should:


*

*define two classes of objects, one "labeled" and the other "unlabeled," where "unlabeled" basically means a class of labeled objects equivalent up to some notion of automorphism;

*write down a logic that allows you to express properties of labeled objects, and another "choiceless logic" that allows you to express properties of the unlabeled objects "without choosing a labeling";

*show that there is some property of labeled objects that is invariant under automorphism but that is inexpressible in your "choiceless logic."
A: In topology, many maps are only characerized by homotopy properties. Proving that a certain homotopy class exists often requires the construction of an actual element in it, and this element is typically not uniquely determined. Aa advanced jargon phrase is that a ''construction depends on a contractible space of choices''. Here are two examples.
If $P \to X$ is a $G$-principal bundle, a ''classifying map'' $f: X \to BG$ is characterized by the property that $f^{\ast} EG \cong BG$, and this is unique up to homotopy. What one does is to prove that the space of $G$-equivariant maps $g:P \to EG$ is contractible (if $X$ is paracompact). Any such $g$ descends to a classifying map $X \to BG$ (and any classfying map is covered by such a $g$). Therefore, $f$ depends on a contractible space of choices and is therefore unique up to homotopy in the strongest possible sense. The concrete construction depends on data such as local trivializations of the bundle and partitions of unity and is therefore not unique or ''natural'' or ''canonical''.
The other example I want to mention is the Pontrjagin-Thom isomorphism, both of whose direction depend on choices. It states a bijection of the set of bordism classes of framed $n$-manifolds in $R^{m+n}$ and homotopy classes of maps $S^{m+n} \to S^m$.
Only after descending to discrete invariants (homotopy and bordism groups), the construction is well-defined. Passing from a bordism class to a homotopy class requires choosing an embedding of the manifold into a euclidean space and the choice of a tubular neighborhood and the choice of a concrete framing. In the reverse direction, you need a representative of the homotopy class by a smooth map and a regular value. 
A: I think that the fundamental group of a path-connected space is an archetype of the phenomenon which you are describing. Its construction and definition requires a choice of basepoint ("Give me a place to stand, and I will move the world", as Archemedes said, quoted by Pappus), but it is independent of that choice up to automorphism (and it's only ever considered up to automorphism).
The "choiceless" object is the fundamental groupoid, but because groupoids are more complicated less familiar algebraic objects than groups, fundamental groups are much more commonly used... and they can't be defined without an arbitrary choice which they are independent of. We just need "a place to stand", that's all!
Philosophically, I think that the reason that we see examples of this phenomenon so often in topology (choice of basepoint, triangulation, smooth structure, lift, cell decomposition, Morse function, etc. where everything is independent of these choices) is that, by definition, manifolds (and, in a weaker sense, other commonly-studied classes of spaces such as CW complexes) "look the same" around any point. So in order to "nail down" a mathematical statement, sometimes we need to "stand somewhere", "introduce coordinates", "fix an arbitrary construction of the space"... and then we can translate our problem to a tractable and/or familiar algebraic category such as "groups", "modules", "symmetric monoidal something", or whatever. These "translations" are the subject of algebraic topology.
A: The simple groups appearing in a composition series of a finite group are independent of the choice of composition series by the Jordan–Hölder theorem, but I'm not aware of a way to define these groups that doesn't involve a choice of composition series. 
A: Daniel Moskovich's notion of "support point" to anchor definitions on manifolds is interesting. I suggest a radically non-geometric example: MATROIDS.
A finite matroid is a finite set with a family of subsets satisfying a list of properties. There are different lists of properties. The subsets could be independent sets, bases, circuits, flats, etc.
Given a matroid defined by independent sets (say) there is a canonical way to find a family of subsets that form a basis (say). So the cool thing about this example is that to define a matroid you need a choice of definition.
A: I think your question can be unasked (in the sense of Gödel-Escher-Bach): The answer depends on what you consider to be a definition - you can describe a mathematical object by its desired properties ~ or give an explicit implementation.
As an example consider the real numbers. An explicit implementation would be to take the rationals and show the Dedekind cuts to be a field. Then call it $\mathbb{R}$ and continue to investigate it using this implementation.
On the other side you can prove the following theorem:

There is an ordered field
  $\mathbb R$ such that every subset
  with a lower bound has an infimum. Every other ordered field $\mathbb R'$ with this property is uniquely isomorphic to $\mathbb R$.

Now the theorem consists of two parts: First a description of the desired properties (ordered, infima) and the uniqueness and second a statement about the existence. In order to show the existence one has to give an explicit imlementation of an object with the desired properties. In our example take the Dedekind cuts.
For the uniqueness part one should be able to work without an explicit implementation, using only the properties. In our case the argument goes as follows: ordered fields have characteristic 0 so we can embed $\mathbb Q$ into both $\mathbb R$ and $\mathbb R'$. Now use the existence of infima of subsets with a lower bound to construct the mapping. There is no need to refer to the Dedekind cuts in this part of the proof.
Back to your question: The crucial distinction is between description and implementation. For example there are several algorithms to sort a list: They are all implementations of the same function - "same" in the sense of extensionality. Likewise there are different ways to build the real numbers - yet they all result in the same object; "same" in the sense specified above.
If one implements an object explicitly making some choices and later on shows that it is "independent" of these choices one has to say what "independent" means in this context. This can only be done by listing properties of the object that characterise it up to some notion of equivalence.
I personally prefer definitions via descriptions: For me $\mathrm{Ext}$ "is" the derived $\mathrm{Hom}$-functor.
PS: I guess the uniqueness of an object up to [some notion of equivalence] can be seen as some sort of extensional equality (in the sense of the yoneda lemma?). I guess Homotopy Type Theory deals with this question but I don't know enough about it to say more in this direction.
A: You can define $\mathrm{Ext}^n$ as the set of isomorphism classes of $n$-step extensions, equipped with the Baer sum.  This eliminates choices from the definition of $\mathrm{Ext}$ in exactly the same spirit as your original post eliminates choices from the definition of the trace.
A: The growth rate of a group, and in particular the notions of polynomial/subexponential growth, are defined in terms of (the Cayley graph corresponding to) a symmetric generating set, but are independent of the symmetric generating set chosen. 
A: I think homology theory is a good example of this phenomenon.  Namely, to construct the simplicial homology groups it is necessary to first choose a triangulation of the space.  In the end, it turns out that the groups are independent of the choice of triangulation, but this is not obvious from first principles.  
A posteriori, the better (choiceless) object that one should work with are the singular homology groups.    
A: The dimension of a vector space is defined to be the size of a basis.
The canonical divisor is defined to be the divisor of a top-degree form.
