Oriented time-oriented orthonormal frame bundle

For each point $p$, use [F1] to choose a neighborhood $U$ and a smooth future-directed tetrad $E$ there. Take any coordinate chart around $p$. Relative to its coordinate determinant frame, the smooth orientation ray [F2] has locally constant sign; shrink around $p$ to keep that sign fixed, and reverse one coordinate if the sign is negative. This gives a local oriented coordinate frame. In it, the determinant of the component matrix of $E$ is a smooth nonzero real function; shrink $U$ to a connected neighborhood of $p$, so its sign is constant. If that sign is negative, replace $E_1$ by $-E_1$. This preserves orthonormality and the future direction of $E_0$ and makes $E$ positively oriented by [F2]. Thus positively oriented future tetrads exist locally.

Let $u,v$ lie in a common fiber of $P_g^{+}(M)$. Since $u$ is an isomorphism, $A:=u^{-1}v$ is the unique real matrix with $v=u\circ A$. The isometry condition gives $A^{\mathsf{T}}\eta A=\eta$. Positivity of the two frame orientations gives $\det A>0$, while the Lorentz identity gives $\det A=\pm 1$, hence $\det A=1$. Because $u(e_0)$ and $v(e_0)$ are future timelike, $A{e}_0$ is future timelike; and the invertible Lorentz map $A$ is a homeomorphism of the timelike set. It therefore maps each connected component onto a component, and the image of $e_0$ shows that it preserves the future component. Thus $A\in S{O}^{+}(1,3)$. This proves that the right action is transitive on each fiber; uniqueness of $A$ proves freeness.

For a local positively oriented future tetrad section $E$ on $U$, define ${\mathrm{\Psi }}_E:U\times S{O}^{+}(1,3)\to (P_g^{+}(M)){\mathrm{\mid }}_U$ by ${\mathrm{\Psi }}_E(p,A)=E(p)\circ A$. Step 1.2 makes this map bijective. Its set-theoretic inverse sends a frame $u$ over $p$ to $(p,E(p{)}^{-1}\circ u)$. We construct the topology and smooth structure using these bijections, rather than assuming smoothness of functions on the total space.

If $E^{\mathrm{\prime }}$ is another such section on an overlap, write $E^{\mathrm{\prime }}(p)=E(p)\circ A(p)$. Its coefficients are $A^I{}_J(p)=e_p^I(E_J^{\mathrm{\prime }}(p))$, hence are smooth functions of the base point: both $e$ and $E^{\mathrm{\prime }}$ are smooth fields on $M$. Thus $A$ is a smooth map into the embedded matrix Lie group [F4], and step 1.2 places every value in $S{O}^{+}(1,3)$. The transition between the charts is $(p,B)\mapsto (p,A(p)B)$, which is smooth; its inverse $(p,B)\mapsto (p,A(p{)}^{-1}B)$ is smooth because inversion is smooth in the Lie group of [F4]. Declare a subset of the total space open exactly when its preimage under every ${\mathrm{\Psi }}_E$ is open. The overlap maps just computed are diffeomorphisms on open product domains, so each ${\mathrm{\Psi }}_E$ is a homeomorphism onto an open subset; combined with base and group coordinate charts, they give a compatible smooth atlas. In this atlas the right action is $(p,B,C)\mapsto (p,BC)$, hence smooth, and the projection is the product projection.

The charts of step 2.1 and smooth transitions from step 3.1 give $P_g^{+}(M)$ local products $U\times S{O}^{+}(1,3)$. Different base points separate by the Hausdorff base [F6], and distinct frames over one point separate in the Hausdorff matrix group [F4], so the total space is Hausdorff. For second countability, let $\mathcal{B}$ be a countable base of $M$; for each $B\in \mathcal{B}$ contained in at least one local-section neighborhood, use [A1] to select one pair consisting of such a neighborhood and a positively oriented future tetrad on it. The selected countable family of neighborhoods covers $M$, and countable bases of each selected $U\times S{O}^{+}(1,3)$ give a countable base of the total space by [F4,F6]. Thus the local charts define a smooth manifold structure. Freeness and fiberwise transitivity were proved in step 1.2; by [F5], this is a smooth right principal $S{O}^{+}(1,3)$-bundle. The construction supplies local sections only, so no global tetrad is asserted.