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.
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$.