PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Compact Lie-group actions are proper

Statement

Every continuous action of a compact Lie group $G$ on a Hausdorff locally compact manifold $M$ is proper: its action-graph map $Θ (g, x) = (g \cdot x, x)$ has compact inverse images of compact sets. In particular, every smooth action of a compact Lie group is proper in the sense of Free and proper Lie-group actions.

Facts & Assumptions

Given: A compact Lie group $G$ , a Hausdorff locally compact manifold $M$ , and a continuous action $G \times M \to M$ .

[F1]

The action is proper exactly when $Θ : G \times M \to M \times M$ , $Θ (g, x) = (g \cdot x, x)$ , has compact inverse images of compact subsets. Free and proper Lie-group actions.

[F2]

The continuous image of a compact subset is compact. A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism.

[F3]

Finite products of compact spaces are compact. A product of finitely many compact spaces is compact in the product topology.

[F4]

A compact subset of a Hausdorff space is closed, and a closed subset of a compact space is compact. In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact.

[F5]

A finite product of Hausdorff spaces is Hausdorff. Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness.

Proof

technique · direct compactness argument

1.1

Let $K \subseteq M \times M$ be compact and let $D = {pr}_{2} (K)$ . The projection is continuous, so $D$ is compact by [F2].

givenF2

2.1

Since both coordinates of every $(g, x) \in Θ^{- 1} (K)$ satisfy $(g \cdot x, x) \in K$ , its second coordinate $x$ lies in $D$ . Hence $Θ^{- 1} (K) \subseteq G \times D$ , and $G \times D$ is compact by [F3].

step 1.1F3

3.1

The manifold $M$ is Hausdorff by hypothesis, so $M \times M$ is Hausdorff by [F5]. Thus $K$ is closed by [F4]. The map $Θ$ is continuous because the action and the second projection are continuous, so $Θ^{- 1} (K)$ is closed in $G \times M$ , and therefore also closed in the subspace $G \times D$ .

givenF4F5step 1.1step 2.1

4.1

By [F4], the closed subset $Θ^{- 1} (K)$ of the compact space $G \times D$ is compact. Since $K$ was arbitrary, [F1] proves properness. Local compactness of $M$ is part of the stated manifold context but is not needed in this compact-domain argument; no freeness or choice principle is used.

F1F4step 2.1step 3.1∎

Depends on

Used by

A proper nonfree action is not a principal bundle Counterexample

Dependency tree · two levels

44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)