Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Lie subgroup–Lie subalgebra correspondence

Statement

Assume ACω. If G is a Lie group and hLie(G) is a Lie subalgebra, there is a connected immersed Lie subgroup i:HG whose identity differential identifies Lie(H) with h. It is unique up to the unique Lie-group isomorphism commuting with the two inclusions into G.

Equivalently, connected immersed Lie subgroups of G, understood together with their intrinsic smooth structures, correspond bijectively to Lie subalgebras of Lie(G).

The assumption ACω is used exactly through the maximal-leaf theorem's construction of a countable leaf atlas and its countable unions.

Facts & Assumptions

Given: ACω, a Lie group G with identity e, and a Lie subalgebra hg=Lie(G).

[A1]

ACω is countable choice. The Axiom of Countable Choice (ACω).

[F1]

The distribution Dg=d(Lg)eh is involutive, and the Frobenius theorem therefore makes it integrable. A Lie-subalgebra distribution is involutive. Frobenius local coordinate theorem.

[F2]

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.

[F3]

Under left translation, Dg=d(Lg)eh satisfies d(La)gDg=Dag. The left-translated distribution associated to a Lie subalgebra.

[F4]

A smooth map with invertible differential at a point is a local diffeomorphism there. The smooth inverse function theorem on manifolds.

Proof

technique · direct construction and uniqueness
1.1

By [F1] and [F2], let H be the maximal connected integral leaf of D through e, with its intrinsic leaf manifold structure and injective immersion i:HG. Its tangent space at e is De=h.

A1F1F2construct
2.1

For every hH, [F3] makes Lh a diffeomorphism preserving D in both directions. It therefore carries the maximal connected integral leaf H to a maximal connected integral leaf Lh(H): any larger connected integral manifold containing Lh(H) would pull back under Lh1 to one properly containing H. But Lh(H) contains h=Lh(e), which belongs to H, so uniqueness of the maximal leaf through h in [F2] gives Lh(H)=H. Hence hhH for h,hH, and because eLh(H) there is hH with hh=e, so h1H. Thus the leaf is a subgroup of G.

F2F3step 1.1algebra
3.1

The ambient division map δ:G×GG, δ(a,b)=ab1, is smooth, and by step 2.1 its restriction to the smooth manifold H×H has image setwise in H. 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 U for D. The leaf H has a countable plaque atlas by [F2]; each atlas plaque meets U in at most countably many connected components, and each such component lies in one U-plaque by the local plaque lemma used in [F2]. Under [A1], HU is therefore a countable union of U-plaques. Near any (a,b)H×H, choose a connected source chart C whose ambient division image is contained in U. The transverse coordinate of δ(C) is a continuous image of connected C 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 δ(C) lies in the single plaque through ab1. Its longitudinal coordinates are smooth as ambient coordinates of δ, giving a smooth H-valued factor in that plaque chart. Hence division is smooth locally everywhere; inversion b1=δ(e,b) and then multiplication ab=δ(a,b1) are smooth. Thus H is a Lie group and i is a smooth injective homomorphism and immersion.

A1F1F2step 1.1step 2.1constructalgebra
4.1

The identity differential of i has image TeH=h by step 1.1, so the constructed immersed subgroup has the required Lie algebra. This also covers h=0, when the connected leaf is {e}, and h=g, when the leaf is the identity component of G.

step 1.1step 3.1algebra
4.2

Let j:KG be any connected immersed Lie subgroup whose tangent algebra is the same h. Translation in K shows dj(TkK)=Dj(k), so j is a connected integral immersion through e. The factorization clause of [F2] gives a unique smooth map f:KH with if=j; injectivity of i and the homomorphism law for j make f a homomorphism. Its identity differential is an isomorphism because both tangent images are h, so [F4] makes f(K) contain an open identity neighborhood in H.

F2F3F4step 1.1step 3.1
5.1

The image f(K) is a subgroup. Since it is open, all its left cosets are open, so its complement is open as well; connectedness of H forces f(K)=H. Injectivity of i and if=j forces f to be injective. Translation of the isomorphism dfe shows that df is invertible everywhere, so [F4] makes f a bijective local diffeomorphism and hence a Lie-group isomorphism; uniqueness follows again from injectivity of i.

F4step 4.2algebra
6.1

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.

A1F1F2F4step 1.1step 2.1step 3.1step 4.1step 4.2step 5.1

Depends on

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