Show that Mat$_{n\times k}^k\to G_k(\mathbb{R}^n)$ is a fibration

Question

I am trying to show that Mat$_{n\times k}^k\to G_k(\mathbb{R}^n)$ is a fibration where Mat$_{n\times k}^k$ denotes the full-rank matrices of rank $k$. I know that $V_k(\mathbb{R}^n)\to G_k(\mathbb{R}^n)$ is a fibration and composition of fibrations is a fibration by Composition and Product of fibrations, so how can we show that Mat$_{n\times k}^k\to V_k(\mathbb{R}^n)$ is a fibration? Also, by Ehresmann's Theorem, every proper submersion is a fibration. The map is indeed a submersion, but I do not think it is proper, so the theorem is not applicable here.

Answer 1

I cannot comprehend this in terms of matrices. Therefore, let $V$ be an $n$-dimensional $\mathbb R$-vector space and let $W\subset V$ be a $k$-dimensional sub-space. Recall that $\mathop{Grass}(k,V)$ is the homogeneous space $\mathop{GL}(V)/H$ with respect to the smooth and transitive action of $\mathop{GL}(V)$ on $\mathop{Grass}(k,V)$ taking sub-spaces to their image under the respective automorphism; i.e., $$H=\mathop{stab}\nolimits_{\mathop{GL}(V)}([W])=\{f\in \mathop{GL}(V)\mid f(W)=W\}.$$

In particular, $\mathop{GL}(V)\to \mathop{Grass}(k,V)$ is a principal $H$-bundle.

The idea is to use the fact that for any closed normal sub-group $H' < H$, the associated $H/H'$-bundle $\mathop{GL}(V)\times_H(H/H')\to\mathop{Grass}(k,V)$ is, by construction, a fibre-bundle. We just have to find the correct $H'$.

Note that $\mathop{GL}(V)$ acts smoothly and transitively on the the space of injective linear maps $\mathop{Inj}(W,V)$ (which is the coordinate-free version of $\mathrm{Mat}^k_{n\times k}$ in this setup) via post-composition. Therefore, $\mathop{Inj}(W,V)$ is the homogeneous space $\mathop{GL}(V)/H'$ where $H'\colon=\{f\mid f|_W=i_W\}\subset \mathop{GL}(V)$ is the stabiliser of the trivial inclusion $i_W\colon W\hookrightarrow V$.

It is easily seen that $H'$ is indeed normal in $H$; thus, $$\mathop{GL}(V)\times_H(H/H')\cong \mathop{GL}(V)/H'\cong \mathop{Inj}(W,V).$$ That this diffeomorphism is compatible with the respective maps onto the Grassmannian is also easy to check.