We consider the minimization problem corresponding to a Sobolev inequality for vector fields and show that minimizing sequences are relatively compact up to the symmetries of the problem. In particular, there is a minimizer. An ingredient in our proof is a version of the Rellich–Kondrachov compactness theorem for sequences satisfying a nonlinear constraint.