Showing that the set of semi-orthogonal matrices is a $C^\infty$ submanifold For $k, n \in \mathbb{N}$ with $k ≤ n$, we define 
$$S_{n, k} = \{X \in \mathbb{R}^{n \times k}: X^t X = I_k\}$$
where $I_k$ is the identity matrix of rank $k$.
I want to prove that $S_{n, k}$ is a $C^\infty$-submanifold of the $\mathbb{R}^{n \times k}$, and want to find it's dimension. Using that, I want to conclude that $S_{n, k}$ is compact.
Now I thought about considering the mapping $f: \mathbb{R}^{n \times k} \to \mathbb{R}^{k \times k}, X \mapsto X^t X - I_k$. Then $S_{n, k}$ would be exactly the set of matrices that $f$ sends to $0$, and $\mathbb{R}^{k \times k} \cong \mathbb{R}^{k^2}$ has dimension $k^2$ whereas $\mathbb{R}^{n \times k}$ is of dimension $nk$, hence, the dimension of $S_{n, k}$ should be $(n - k)k$, I believe?
However, I still need to show that $f$ is not only continuously differentiable once and has a Jacobean matrix of proper rank (which would give me that $S_{n, k}$ is a $C^1$ manifold, I believe, since every $X \in S_{n, k}$ is a regular point then), but infinitely often, in order for $C^\infty$, do I? (Or is there an easier way?) And I don't really know how to get started with that.
Alternatively, I know I could also find a chart and show that it's $C^\infty$, but I don't know if that's easier either.
Thanks in advance.
EDIT: It also came to my mind that a chart might even be the more handier thing, since I'm supposed to conclude that $S_{n, k}$ is compact. Because the way the exercise is proposed makes it look like I'm supposed to use a topology argument, e.g. something like "$S_{n, k}$ is compact as the image of a compact space regarding a homeomorphism/diffeomorphism". I'm not sure though, and I'm of course open to all different kinds of approaches.
 A: Your approach is good, but it is important to choose the appropriate target set for $f$. We better consider $f$ as a map between $\mathbb{R}^{n\times k}$ and the set of symmetric $k\times k$ matrices (which has dimension $k(k+1)/2$). This will allow you to show that $0$ is a regular value of $f$, as follows:    
You can check that the derivative $d_{X}f(Y)$ is given by $X^{T}Y+Y^{T}X$. We choose $X\in f^{-1}(0)$ and show that $d_{X}f$ is surjective (for this, the choice of the target set of $f$ is important). Take a symmetric $k\times k$ matrix $B$. Then we have
$d_{X}f(\frac{1}{2}XB)=\frac{1}{2}X^{T}XB+\frac{1}{2}B^{T}X^{T}X=\frac{1}{2}B+\frac{1}{2}B^{T}=B$.
Hence, $S_{n,k}$ will be a submanifold of $\mathbb{R}^{n\times k}$ of dimension $nk-k(k+1)/2$.
A: You don't need this result for proving that your set is compact.
In fact, set $S_{n,k}$ is defined by a system of $k^2$ equations 
$$(E_{pq}:) \ \ \ \sum_{i=1}^n x_{pi}x_{qi}=\delta_{pq}$$
(where $\delta_{pq}$ is the Kronecker symbol: $1$ if $p=q$, $0$ otherwise).
Edit (following a remark of Moran pointing to a deficiency in my reasoning):
In particular, if we add the constraints corresponding to the cases $\delta_{pp}=1$, we obtain the fact that the sum of the squares of all entries of $X$ is $1+1+...1=k$, proving that the set $S_{n,k}$ is included into the sphere $S$ of $\mathbb{R}^{n \times k}$ with radius $\sqrt{k}$, which is a compact set (it is a characteristic of finite dimensional spaces). Remark: using Frobenius norm, this constraint could be written $\|X\|_F^2=k$.
Each constraint $(E_{pq})$ defines a subset $E_{pq}$ of $\mathbb{R}^{n \times k}$ expressed as a certain $f_{pq}^{-1}\{a\}$ ($a=0$ or $1$) where $f_{pq}$ is continuous (even much more than that...). 
Thus, $E_{pq}$, being the reciprocal image of a compact set (here $\{0\}$ or $\{1\}$) by a continuous function from the compact set $S$ (defined upwards) to $\mathbb{R}$, is itself a compact set. Inverse image of a compact set is compact
The intersection of these compact sets $E_{pq}$ is a compact set: we have reached the final objective.
