TheoremStatement: AI-adaptedProof: 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.

One-parameter subgroups are integral curves of left-invariant fields

Statement

Assume ${A C}_{ω}$ . Let $G$ be a finite-dimensional real Lie group with Lie algebra $g = T_{e} G$ .

If $γ : R \to G$ is a one-parameter subgroup and $X = γ^{'} (0)$ , then

$γ^{'} (t) = d (L_{γ (t)})_{e} X = X_{γ (t)}^{L}$

for every $t \in R$ ; thus $γ$ is the integral curve through $e$ of the left-invariant field $X^{L}$ . Conversely, the global integral curve through $e$ of $X^{L}$ is a one-parameter subgroup. Consequently every $X \in g$ determines a unique one-parameter subgroup with initial velocity $X$ .

The countable-choice assumption is used exactly through the supplied smooth invariant-field construction and completeness theorem.

Facts & Assumptions

Given: ${A C}_{ω}$ , a finite-dimensional real Lie group $G$ with identity $e$ , and $X \in g = T_{e} G$ .

[F1]

${A C}_{ω}$ is countable choice. The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F2]

A one-parameter subgroup is a smooth homomorphism $γ : (R, +) \to G$ , so $γ (s + t) = γ (s) γ (t)$ and $γ (0) = e$ . One-parameter subgroup of a Lie group.

[F3]

Evaluation at $e$ identifies $g$ with the left-invariant smooth fields: $X$ determines the unique field $X_{g}^{L} = d (L_{g})_{e} X$ . This result assumes ${A C}_{ω}$ through the smooth tangent-bundle framework. Left-invariant vector fields evaluate isomorphically at the identity.

[F4]

Every left-invariant smooth field is complete, assuming ${A C}_{ω}$ through that same framework. Left-invariant vector fields are complete.

[F5]

A curve $c$ is an integral curve of a field $Y$ precisely when $c^{'} (t) = Y_{c (t)}$ . Integral curves of a vector field.

[F6]

Through each point there is a unique maximal integral curve. Through each point there is a unique maximal integral curve.

[F7]

Differentials of smooth maps obey the chain rule. The chain rule for differentials of smooth maps.

Proof

technique · direct

1.1

Let $γ$ be a one-parameter subgroup with $γ^{'} (0) = X$ . For fixed $t$ , [F2] gives $γ (t + s) = L_{γ (t)} (γ (s))$ . Differentiating at $s = 0$ and using [F7] yields $γ^{'} (t) = d (L_{γ (t)})_{e} γ^{'} (0) = d (L_{γ (t)})_{e} X = X_{γ (t)}^{L} .$ Hence $γ$ is an integral curve of $X^{L}$ through $e$ .

F2F3F5F7algebra

1.2

Conversely, let $X^{L}$ be the unique field supplied by [F3]. By [F4] and [F6], its maximal integral curve $c : R \to G$ with $c (0) = e$ is global. Fix $s \in R$ and define $a_{s} (t) = c (s + t)$ and $b_{s} (t) = c (s) c (t)$ . Both curves are defined for every real $t$ , and $a_{s} (0) = b_{s} (0) = c (s)$ .

F3F4F6construct

2.1

By [F5], $a_{s}^{'} (t) = X_{c (s + t)}^{L} = X_{a_{s} (t)}^{L}$ . The chain rule and left invariance give $b_{s}^{'} (t) = d (L_{c (s)})_{c (t)} c^{'} (t) = d (L_{c (s)})_{c (t)} X_{c (t)}^{L} = X_{c (s) c (t)}^{L} = X_{b_{s} (t)}^{L} .$ Thus $a_{s}$ and $b_{s}$ are global integral curves through the same point at time zero. Uniqueness in [F6] gives $c (s + t) = c (s) c (t)$ for all $s, t \in R$ .

F3F5F6F7step 1.2algebra

3.1

The curve $c$ is smooth, global, satisfies $c (0) = e$ and the homomorphism law from step 2.1, so it is a one-parameter subgroup by [F2]; its initial velocity is $c^{'} (0) = X_{e}^{L} = X$ . If $γ$ is any other one-parameter subgroup with initial velocity $X$ , step 1.1 makes it an integral curve of $X^{L}$ through $e$ , and [F6] forces $γ = c$ . This proves existence and uniqueness for every $X \in g$ .

F2F3F5F6step 1.1step 2.1

4.1

Lie groups are nonempty and boundaryless. If $\dim G = 0$ , then $X = 0$ and the unique curve is constant; in dimension one the proof is unchanged. Both time directions are covered because $c$ has domain all of $R$ . No metric or nondegeneracy condition occurs. The only choice assumption is the stated ${A C}_{ω}$ , inherited through [F3] and [F4]; fixing one $X$ and one real $s$ adds no family choice. The two implications in the statement are proved in steps 1.1 and 1.2--3.1.

F1F2F3F4F5F6F7step 1.1step 1.2step 2.1step 3.1∎

Depends on

Used by

Exponential map of a Lie group Definition
Right-trivialized differential of the Lie-group exponential Lemma
Commuting Lie-algebra elements have multiplicative exponentials Proposition
Exponential scales one-parameter subgroups Proposition
Baker–Campbell–Hausdorff theorem Theorem
One-parameter subgroups are exactly exponentials Theorem
The differential of Ad is ad Theorem
The Lie-group exponential map is smooth with identity differential at zero Theorem

Dependency tree · two levels

22 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

Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)