LemmaStatement: AI-adaptedProof: AI-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Quotients of Lorentzian manifolds by free proper isometric discrete actions

Statement

Let $(\hat{M}, \hat{g})$ be a smooth Lorentzian four-manifold (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Smooth covariant 2-tensor fields on a smooth manifold), let $Γ$ be a discrete group equipped with its discrete smooth structure (a zero-dimensional Lie group, so that a smooth action is one for which every map $p \mapsto γ \cdot p$ , $γ \in Γ$ , is smooth), and let $Γ$ act on $\hat{M}$ smoothly, freely and properly in the sense of Free and proper Lie-group actions; write $γ \cdot p$ for the action and $d γ_{p}$ for the differential of $p \mapsto γ \cdot p$ (The differential of a smooth map). Suppose that every $γ \in Γ$ preserves $\hat{g}$ , that is ${\hat{g}}_{γ \cdot p} (d γ_{p} V, d γ_{p} W) = {\hat{g}}_{p} (V, W)$ for all $p \in \hat{M}$ , $V, W \in T_{p} \hat{M}$ and $γ \in Γ$ . Let $q : \hat{M} \to M : = \hat{M} / Γ$ be the orbit map. Then:

(a) $M$ is a Hausdorff second-countable smooth four-manifold, $q$ is a smooth surjective submersion, and $q$ is a local diffeomorphism at every point of $\hat{M}$ .

(b) There is a unique smooth Lorentzian metric $g$ of signature $(-, +, +, +)$ on $M$ with $q^{*} g = \hat{g}$ ; equivalently $g_{q (p)} (d q_{p} V, d q_{p} W) = {\hat{g}}_{p} (V, W)$ for all $p, V, W$ .

(c) If $\hat{N}$ is a smooth vector field on $\hat{M}$ (A smooth vector field is a smooth section of the tangent bundle) which is $Γ$ -invariant, ${\hat{N}}_{γ \cdot p} = d γ_{p} ({\hat{N}}_{p})$ , and satisfies $\hat{g} (\hat{N}, \hat{N}) < 0$ , then the prescription $N_{q (p)} : = d q_{p} ({\hat{N}}_{p})$ defines a smooth vector field $N$ on $M$ with $g (N, N) < 0$ for all points. In particular, a $Γ$ -invariant time orientation of $(\hat{M}, \hat{g})$ descends to one of $(M, g)$ .

Facts & Assumptions

Given: A smooth Lorentzian four-manifold $(\hat{M}, \hat{g})$ , a discrete group $Γ$ acting smoothly, freely, properly and preserving $\hat{g}$ , and the orbit map $q$ .

[L1]

The quotient $M = \hat{M} / Γ$ of a smooth free proper action of a Lie group is a Hausdorff second-countable smooth manifold, and $q$ is a smooth surjective submersion (Free proper action quotient manifold, Free and proper Lie-group actions).

[L2]

The discrete group $Γ$ is zero-dimensional, so the dimension statement of [L1] gives $\dim M = \dim \hat{M} - 0 = 4$ .

[L3]

A smooth map between smooth manifolds whose differential is invertible at every point is a local diffeomorphism: around every point it restricts to a diffeomorphism onto an open image, with a smooth inverse (The smooth inverse function theorem on manifolds).

[L4]

The orbit map satisfies $q \circ γ = q$ for every $γ \in Γ$ , hence $d q_{γ \cdot p} \circ d γ_{p} = d q_{p}$ wherever the differentials are formed (The differential of a smooth map).

[L5]

A smooth cocycle identity such as ${\hat{g}}_{γ \cdot p} (d γ_{p} V, d γ_{p} W) = {\hat{g}}_{p} (V, W)$ for all $p$ uses only the differentials; it implies the same identity for all smooth vector fields along the orbit (The differential of a smooth map, Smooth covariant 2-tensor fields on a smooth manifold).

Proof

technique · direct

1.1givenL1L2L3

(The quotient and local diffeomorphism property.) By [L1] and [L2], $M$ is a Hausdorff second-countable smooth four-manifold and $q$ is a smooth surjective submersion. Since $\dim M = \dim \hat{M}$ , the differential $d q_{p} : T_{p} \hat{M} \to T_{q (p)} M$ is a linear isomorphism for every $p$ : it is onto by the submersion property and the spaces have the same finite dimension. By [L3] every point of $\hat{M}$ has an open neighborhood $\hat{U}$ such that $q ∣_{\hat{U}} : \hat{U} \to q (\hat{U})$ is a diffeomorphism onto an open set; in particular there are smooth local sections $s : V \to \hat{M}$ with $q \circ s = {id}_{V}$ over open sets $V \subseteq M$ covering $M$ . This proves (a).

2.1step 1.1givenL4L5

(The metric: well-definedness.) For $r \in M$ and $v, w \in T_{r} M$ choose $p \in q^{- 1} (r)$ and the unique $\hat{V}, \hat{W} \in T_{p} \hat{M}$ with $d q_{p} \hat{V} = v$ , $d q_{p} \hat{W} = w$ , and set $g_{r} (v, w) : = {\hat{g}}_{p} (\hat{V}, \hat{W})$ . To see that this is independent of the choice of $p$ : if $p^{'} = γ \cdot p$ , then by [L4] and the injectivity of $d q_{p^{'}}$ the unique preimage of $v$ at $p^{'}$ is $d γ_{p} \hat{V}$ , and similarly for $w$ , so the defining cocycle identity of the statement gives ${\hat{g}}_{p^{'}} (d γ_{p} \hat{V}, d γ_{p} \hat{W}) = {\hat{g}}_{p} (\hat{V}, \hat{W})$ . The assignment is symmetric and bilinear in $(v, w)$ at each $r$ because ${\hat{g}}_{p}$ is, and it is nondegenerate with signature $(-, +, +, +)$ because $d q_{p}$ is a linear isomorphism and ${\hat{g}}_{p}$ is nondegenerate of that signature (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

3.1step 1.1step 2.1given

(Smoothness and uniqueness.) Let $s : V \to \hat{M}$ be a smooth local section of $q$ as in step 1.1. For $r \in V$ and $v, w \in T_{r} M$ one has $d q_{s (r)} \circ d s_{r} = {id}_{T_{r} M}$ , so $g_{r} (v, w) = {\hat{g}}_{s (r)} (d s_{r} v, d s_{r} w)$ , that is, $g ∣_{V} = s^{*} \hat{g}$ . Both $s$ and $\hat{g}$ are smooth, so the components of $g$ in any chart contained in $V$ are smooth; since the open sets $V$ cover $M$ , $g$ is a smooth covariant $2$ -tensor field on $M$ (Smooth covariant 2-tensor fields on a smooth manifold). If $g^{'}$ were another smooth metric with $q^{*} g^{'} = \hat{g}$ , then for every $r$ , $v, w$ and choice of $p$ , $\hat{V}, \hat{W}$ as in step 2.1 one would have $g_{r}^{'} (v, w) = {\hat{g}}_{p} (\hat{V}, \hat{W}) = g_{r} (v, w)$ , so $g^{'} = g$ . This proves (b).

3.2step 1.1step 2.1givenL4

(The time orientation.) Let $\hat{N}$ be $Γ$ -invariant with $\hat{g} (\hat{N}, \hat{N}) < 0$ . For $p^{'} = γ \cdot p$ the invariance gives $d γ_{p} {\hat{N}}_{p} = {\hat{N}}_{p^{'}}$ , so $d q_{p^{'}} {\hat{N}}_{p^{'}} = d q_{p^{'}} (d γ_{p} {\hat{N}}_{p}) = d q_{p} {\hat{N}}_{p}$ by [L4]; hence $N_{q (p)} : = d q_{p} {\hat{N}}_{p}$ is well defined on $M$ , and it is smooth because over a local section $s$ it equals $d q_{s (r)} {\hat{N}}_{s (r)} = d s_{r}^{- 1} {\hat{N}}_{s (r)}$ , a smooth expression. Moreover $g (N, N)_{q (p)} = {\hat{g}}_{p} ({\hat{N}}_{p}, {\hat{N}}_{p}) < 0$ by the defining formula of step 2.1; so $N$ is a time orientation of $(M, g)$ in the sense of Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model clause (c).

4.1step 1.1step 2.1step 3.1step 3.2∎

(Conclusion.) Part (a) is step 1.1, part (b) is steps 2.1 and 3.1, and part (c) is step 3.2; this completes the proof.

Remarks

Hypotheses. Freeness and properness are used only through the quotient theorem [L1]; discreteness is used only to make the quotient four-dimensional, so that $q$ is a local diffeomorphism. The metric descent itself uses only invariance under the action and the local-diffeomorphism property.
Scope. The result is a construction of a new Lorentzian model from an old one. It asserts nothing about the causal character of either model; whether the quotient is causal depends on the action and is decided by the properties of the closed orbits, as the flat cylinder example on the companion page shows.

Quotients of Lorentzian manifolds by free proper isometric discrete actions

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources