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.
Lie subgroup–Lie subalgebra correspondence
Statement
Assume . If is a Lie group and is a Lie subalgebra, there is a connected immersed Lie subgroup whose identity differential identifies with . It is unique up to the unique Lie-group isomorphism commuting with the two inclusions into .
Equivalently, connected immersed Lie subgroups of , understood together with their intrinsic smooth structures, correspond bijectively to Lie subalgebras of .
The assumption is used exactly through the maximal-leaf theorem's construction of a countable leaf atlas and its countable unions.
Facts & Assumptions
Given: , a Lie group with identity , and a Lie subalgebra .
is countable choice. The Axiom of Countable Choice ().
The distribution is involutive, and the Frobenius theorem therefore makes it integrable. A Lie-subalgebra distribution is involutive. Frobenius local coordinate theorem.
Every point of an integrable distribution lies on a unique maximal connected integral manifold, and every connected integral immersion through that point factors uniquely and smoothly through it. Existence and uniqueness of maximal connected integral manifolds.
Under left translation, satisfies . The left-translated distribution associated to a Lie subalgebra.
A smooth map with invertible differential at a point is a local diffeomorphism there. The smooth inverse function theorem on manifolds.
Proof
By [F1] and [F2], let be the maximal connected integral leaf of through , with its intrinsic leaf manifold structure and injective immersion . Its tangent space at is .
For every , [F3] makes a diffeomorphism preserving in both directions. It therefore carries the maximal connected integral leaf to a maximal connected integral leaf : any larger connected integral manifold containing would pull back under to one properly containing . But contains , which belongs to , so uniqueness of the maximal leaf through in [F2] gives . Hence for , and because there is with , so . Thus the leaf is a subgroup of .
The ambient division map , , is smooth, and by step 2.1 its restriction to the smooth manifold has image setwise in . Setwise inclusion alone would not prove smoothness for the intrinsic leaf topology. We use the countable-plaque construction in the proof of [F2]. Fix a flat-chart domain for . The leaf has a countable plaque atlas by [F2]; each atlas plaque meets in at most countably many connected components, and each such component lies in one -plaque by the local plaque lemma used in [F2]. Under [A1], is therefore a countable union of -plaques. Near any , choose a connected source chart whose ambient division image is contained in . The transverse coordinate of is a continuous image of connected into the countable set of transverse coordinates of those plaques. A connected countable subset of Euclidean space is a singleton, so this transverse coordinate is constant and lies in the single plaque through . Its longitudinal coordinates are smooth as ambient coordinates of , giving a smooth -valued factor in that plaque chart. Hence division is smooth locally everywhere; inversion and then multiplication are smooth. Thus is a Lie group and is a smooth injective homomorphism and immersion.
The identity differential of has image by step 1.1, so the constructed immersed subgroup has the required Lie algebra. This also covers , when the connected leaf is , and , when the leaf is the identity component of .
Let be any connected immersed Lie subgroup whose tangent algebra is the same . Translation in shows , so is a connected integral immersion through . The factorization clause of [F2] gives a unique smooth map with ; injectivity of and the homomorphism law for make a homomorphism. Its identity differential is an isomorphism because both tangent images are , so [F4] makes contain an open identity neighborhood in .
The image is a subgroup. Since it is open, all its left cosets are open, so its complement is open as well; connectedness of forces . Injectivity of and forces to be injective. Translation of the isomorphism shows that is invertible everywhere, so [F4] makes a bijective local diffeomorphism and hence a Lie-group isomorphism; uniqueness follows again from injectivity of .
The only countable construction is [F2], whose proof spends [A1] on a countable flat-chart cover and countable unions. The countable-plaque argument in step 3.1 uses the same premise and is precisely what makes a setwise leaf-valued smooth map intrinsically smooth. The remaining selections are single finite-dimensional or local choices and use no stronger choice principle. Steps 1.1–4.1 give existence and steps 4.2–5.1 give uniqueness, establishing the stated correspondence.
Depends on
- The left-translated distribution associated to a Lie subalgebra
- A Lie-subalgebra distribution is involutive
- Frobenius local coordinate theorem
- Existence and uniqueness of maximal connected integral manifolds
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The smooth inverse function theorem on manifolds
Used by
Dependency tree · two levels
40 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)
- Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I (standard reference, not scraped)