Alphabeta Math
Pipeline-generated
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.

✓ 39 results · all verified · 37 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Lie Groups, Invariant Fields, and the Exponential Map

1 · Prerequisites

2 · Summary

A Lie group's tangent space at the identity acquires its bracket from left-invariant vector fields; right-invariant fields instead realize the opposite bracket. The left Maurer--Cartan form packages the resulting global trivialization and satisfies the Maurer--Cartan structure equation with this fixed sign convention.

Complete invariant fields produce one-parameter subgroups and the exponential map. The exponential is smooth, has identity differential at zero, and is therefore a local diffeomorphism, but it need not be a homomorphism, globally injective, or globally surjective. Naturality and connectedness determine homomorphisms locally and, where stated, globally. The smooth invariant-field and exponential interfaces on this page explicitly retain ACω.

Conjugation gives the adjoint representation, whose differential is the Lie-algebra adjoint map. The final section proves a local Baker--Campbell--Hausdorff formula from the right-trivialized differential of the exponential. All logarithm and commutation conclusions retain their neighbourhood hypotheses; no global BCH or global logarithm claim is made.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Lie group

Definition

A finite-dimensional real Lie group is a group G, in the sense of Group and abelian group, together with the structure of a finite-dimensional real smooth manifold such that the maps

m:G×G⟶G,m(g,h)=gh,

and

inv⁡:G⟶G,inv⁡(g)=g−1,

are smooth in the sense of Smooth maps between manifolds with boundary. Its identity element is denoted by e (or occasionally 1).

Unless an item explicitly says otherwise, every Lie group on this page is real, finite-dimensional, and has no manifold boundary. Dimension zero is allowed; for example, any countable discrete group with its discrete zero-dimensional smooth structure is a Lie group. A Lie group cannot be empty because a group contains its identity. The definition applies unchanged in dimension one, uses no metric or nondegeneracy hypothesis, and makes no choice from a family of sets.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Lie-group homomorphism, isomorphism, and automorphism

Definition

Let G and H be Lie groups in the sense of Lie group. A Lie-group homomorphism F:G→H is a group homomorphism in the sense of Monoid homomorphism and group homomorphism that is also smooth. Thus

F(gh)=F(g)F(h)

for all g,h∈G, while preservation of identity and inverses follows from the group-homomorphism laws.

A Lie-group isomorphism is a bijective Lie-group homomorphism whose inverse is smooth. Its set-theoretic inverse is automatically a group homomorphism by The inverse of a bijective group homomorphism is a group homomorphism, so the smoothness clause makes that inverse a Lie-group homomorphism as well. A Lie-group automorphism is a Lie-group isomorphism from G to itself.

Smoothness is part of the homomorphism definition on this page. The separate automatic-regularity theorem for merely continuous group homomorphisms is not being assumed. These definitions apply without alteration in dimensions zero and one. Their Lie-group inputs are nonempty and boundaryless by the page convention, and the definitions use neither nondegeneracy nor any choice principle.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Left and right translations on a Lie group

Definition

Let G be a Lie group and fix g∈G. The left translation by g and right translation by g are respectively

Lg:G⟶G,Lg(h)=gh,

and

Rg:G⟶G,Rg(h)=hg.

Both maps are smooth: each is obtained from the smooth multiplication m:G×G→G in Lie group by holding one argument fixed. The notation here is the ordinary right-translation convention. Kirillov writes a right action as h↦hg−1; therefore this page's Rg is that source's right action by g−1.

The definition applies in dimensions zero and one and uses no metric or nondegeneracy condition. A Lie group is nonempty, its manifold is boundaryless by the page convention, and the one supplied element g involves no choice from a family.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Translations are diffeomorphisms and their differentials trivialize the tangent bundle

Statement

Assume ACω. For every g in a Lie group G, the maps Lg and Rg are diffeomorphisms with respective inverses Lg−1 and Rg−1. Moreover,

ΦL:G×TeG⟶TG,ΦL(g,X)=d(Lg)eX,

and

ΦR:G×TeG⟶TG,ΦR(g,X)=d(Rg)eX,

are smooth vector-bundle isomorphisms over id⁡G.

The countable-choice assumption is used exactly through the supplied theorem that equips tangent bundles and global differentials with their smooth structures.

Facts & Assumptions

Given: ACω, a Lie group G with identity e, and g∈G.

[F1]

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

[F2]

Left and right translations are Lg(h)=gh and Rg(h)=hg, and both are smooth. Left and right translations on a Lie group.

[F3]

Assuming ACω, the global differential of a smooth map is smooth between the canonical smooth tangent bundles. Assuming countable choice, the global differential of a smooth map is smooth.

[F4]

The differential of a diffeomorphism is a linear isomorphism on every tangent space. The differential of a diffeomorphism is an isomorphism.

[F5]

A fibrewise bijective smooth bundle map over a diffeomorphism is a vector-bundle isomorphism. A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism.

Proof

technique · direct
1.1F2algebra

The group laws give Lg∘Lg−1=Lg−1∘Lg=id⁡G and Rg∘Rg−1=Rg−1∘Rg=id⁡G. All four translations are smooth by [F2], so Lg and Rg are diffeomorphisms with the asserted inverses.

1.2F1F2F3algebra

Let m:G×G→G be multiplication. Near an arbitrary g0, choose product coordinates in which m is represented by a smooth map μ(a,b). The local matrix of d(Lg)e is the second-variable Jacobian D2μ(a,be), whose entries are smooth in a. Equivalently, this is the restriction of the smooth global differential dm supplied by [F3]. Therefore ΦL is a smooth bundle map. The same calculation with the variables reversed gives smoothness of ΦR.

2.1F4step 1.1

By [F4] and step 1.1, each fibre map d(Lg)e:TeG→TgG and d(Rg)e:TeG→TgG is a linear isomorphism. Hence ΦL and ΦR are fibrewise linear bijections over id⁡G.

3.1F5step 1.1step 2.1step 1.2

Apply [F5] to the smooth fibrewise bijections from steps 2.1 and 1.2 over id⁡G. Both ΦL and ΦR are vector-bundle isomorphisms. Fibrewise, their inverses are (g,V)↦(g,d(Lg−1)gV) and (g,V)↦(g,d(Rg−1)gV), respectively.

4.1F1F2F3F4F5step 1.1step 2.1step 1.2step 3.1∎

A Lie group is nonempty. If dim⁡G=0, all tangent fibres are zero spaces and the displayed maps are the unique fibre maps; if dim⁡G=1, the same proof applies. No metric or nondegeneracy condition occurs, and the group is boundaryless by the page convention. The only choice assumption is the stated ACω, used through [F3] for the canonical smooth tangent bundles/global differential; all group operations and local computations are supplied or pointwise and add no choice. The item asserts explicit inverse identities but no biconditional.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Left- and right-invariant vector fields

Definition

Assume ACω, and let X be a smooth vector field on a Lie group G. The field X is left invariant if

d(Lg)h(Xh)=Xgh

for every g,h∈G. It is right invariant if

d(Rg)h(Xh)=Xhg

for every g,h∈G, where Rg(h)=hg is the ordinary right translation.

In the left-invariant case, setting h=e gives Xg=d(Lg)e(Xe). Conversely, if that identity-value formula holds for every g, then the chain rule and Lg∘Lh=Lgh give

d(Lg)h(Xh)=d(Lg)hd(Lh)e(Xe)=d(Lgh)e(Xe)=Xgh.

Thus left invariance is equivalent to the displayed identity-value formula. Likewise, Rg∘Rh=Rhg shows that right invariance is equivalent to Xg=d(Rg)e(Xe). This agrees with Kirillov's Definition 2.26 after translating the source's inverse-parametrized right action into the ordinary right-translation convention used here.

The assumption ACω is inherited exactly through the supplied definition of a smooth vector field on the canonical smooth tangent bundle and through the supplied translation trivializations. The chain-rule calculation is pointwise and makes no further choice. A Lie group is nonempty; in dimension zero the tangent values are all zero, and the same definition applies in dimension one. No metric or nondegeneracy hypothesis occurs, and Lie groups are boundaryless by the page convention.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Left-invariant vector fields evaluate isomorphically at the identity

Statement

Assume ACω. Let XL(G) and XR(G) be the real vector spaces of left- and right-invariant smooth vector fields on a Lie group G. Evaluation at the identity gives linear isomorphisms

ev⁡eL:XL(G)⟶TeG

and

ev⁡eR:XR(G)⟶TeG.

Their respective inverses send v∈TeG to

vgL=d(Lg)e(v)andvgR=d(Rg)e(v).

The countable-choice assumption is used exactly through the supplied invariant-field and smooth translation-trivialization results.

Facts & Assumptions

Given: ACω, a Lie group G with identity e, and a vector v∈TeG.

[F1]

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

[F2]

Invariance is equivalent to the appropriate identity-value formula. Left- and right-invariant vector fields.

[F3]

The maps (g,v)↦d(Lg)e(v) and (g,v)↦d(Rg)e(v) are smooth vector-bundle isomorphisms. Translations are diffeomorphisms and their differentials trivialize the tangent bundle.

Proof

technique · direct
1.1F2algebra

Pointwise addition and scalar multiplication preserve smooth vector fields. Because each differential d(Lg)h is linear, they also preserve left invariance; the same holds on the right. Thus XL(G) and XR(G) are real vector spaces, and evaluation at e is linear on each.

1.2F2F3algebra

Fix v∈TeG. The map g↦(g,v) is a smooth section of the product bundle G×TeG. Composing it with the left trivialization in [F3] shows that vgL=d(Lg)e(v) is a smooth vector field. Its identity-value formula makes it left invariant by [F2], and veL=d(Le)e(v)=v.

2.1F2step 1.1step 1.2

Conversely, [F2] forces every X∈XL(G) to satisfy Xg=d(Lg)e(Xe) at every g. Hence X=(Xe)L, so v↦vL and ev⁡eL are mutually inverse linear maps.

2.2F2F3step 1.1algebra

Replacing the left trivialization by the right trivialization in [F3] gives a smooth field vgR=d(Rg)e(v). The right identity-value characterization in [F2] proves invariance and uniqueness, while Re=id⁡G gives veR=v. Thus v↦vR is the inverse of ev⁡eR.

3.1F1F2F3step 1.1step 1.2step 2.1step 2.2∎

A Lie group is nonempty. If dim⁡G=0, then TeG=0 and both invariant-field spaces contain only the zero field, so both evaluation maps are the unique zero-dimensional isomorphisms; dimension one needs no change. No metric or nondegeneracy condition occurs, and the group is boundaryless by convention. The stated ACω is inherited through [F2] and [F3]; fixing the supplied vector v and performing pointwise linear operations adds no choice. The theorem asserts two explicit isomorphisms, not a biconditional.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The Lie bracket of left-invariant fields is left invariant

Statement

Assume ACω. If X and Y are left-invariant smooth vector fields on a Lie group G, then their Lie bracket [X,Y] is left invariant.

The countable-choice assumption is used exactly through the supplied invariant-field and smooth translation-trivialization results.

Facts & Assumptions

Given: ACω, a Lie group G, and left-invariant smooth vector fields X,Y on G.

[F1]

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

[F2]

Left invariance means that every left translation carries the field to itself pointwise. Left- and right-invariant vector fields.

[F4]

Pushforward by a diffeomorphism preserves the Lie bracket. Diffeomorphism pushforward preserves Lie brackets.

Proof

technique · direct
1.1F2F3

Fix g∈G. By [F3], Lg is a diffeomorphism. The pointwise invariance identities in [F2] say exactly that (Lg)∗X=X and (Lg)∗Y=Y.

2.1F2F4step 1.1

Naturality [F4] and step 1.1 give (Lg)∗[X,Y]=[(Lg)∗X,(Lg)∗Y]=[X,Y]. Since g was arbitrary, [F2] says that [X,Y] is left invariant.

3.1F1F2F3F4step 1.1step 2.1∎

A Lie group is nonempty. In dimension zero all vector fields and brackets vanish, while dimension one requires no change. No metric or nondegeneracy condition occurs, and the group is boundaryless by convention. The stated ACω is inherited through [F2] and [F3]; fixing one arbitrary group element and applying bracket naturality makes no family selection. The proposition is a one-way closure statement, not a biconditional.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Lie bracket on the tangent space of a Lie group

Definition

Assume ACω, let G be a Lie group with identity e, and write g=TeG. For u,v∈g, let uL and vL be their unique left-invariant smooth extensions. Define the Lie-group tangent bracket by

[u,v]G=[uL,vL]e.

The evaluation isomorphism Left-invariant vector fields evaluate isomorphically at the identity makes both extensions unique, so the definition is unambiguous. Moreover, The Lie bracket of left-invariant fields is left invariant makes [uL,vL] left invariant, and hence its identity value determines it:

[uL,vL]=[u,v]GL.

The bracket on fields is the library's fixed commutator [X,Y]f=X(Yf)−Y(Xf) from The Lie bracket of smooth vector fields. This explicitly fixes the sign for every later occurrence of ad⁡, the Maurer--Cartan equation, and right-invariant fields. In particular, no opposite vector-field commutator convention is being imported from a source.

The assumption ACω is inherited exactly through the supplied invariant-extension and bracket-closure results; evaluating the supplied vector-field bracket at e adds no choice. A Lie group is nonempty. If dim⁡G=0, then g=0 and this is the unique zero bracket; the definition applies unchanged in dimension one. No metric or nondegeneracy hypothesis occurs, and the group is boundaryless by convention.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Finite-dimensional Lie algebra

Definition

Let F be either R or C. A finite-dimensional Lie algebra over F is a finite-dimensional F-vector space g together with an F-bilinear map

[ , ]:g×g⟶g

such that, for all X,Y,Z∈g,

[X,X]=0

and

[X,[Y,Z]]+[Y,[Z,X]]+[Z,[X,Y]]=0.

The first identity is alternation and the second is the Jacobi identity. Over R or C, alternation is equivalent to skew-symmetry. Indeed, bilinearity and alternation give 0=[X+Y,X+Y]=[X,Y]+[Y,X], while skew-symmetry gives 2[X,X]=0 and hence [X,X]=0 because both fields have characteristic zero. For a complex Lie algebra the bracket is required to be complex-bilinear, not merely real-bilinear.

The definition permits the zero bracket. The zero vector space, with its unique bracket, is a zero-dimensional Lie algebra. On a one-dimensional space, every alternating bilinear bracket is zero: any two vectors are scalar multiples of one vector and bilinearity reduces their bracket to [X,X]=0. A vector space is nonempty because it contains zero. No basis is selected by asserting finite-dimensionality, so the definition is choice-free. It is purely algebraic and has no metric, nondegeneracy, manifold-boundary, or endpoint condition.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The tangent space at the identity is a Lie algebra

Statement

Assume ACω. If G is a finite-dimensional real Lie group with identity e, then g=TeG, equipped with the bracket transported from left-invariant smooth vector fields, is a finite-dimensional real Lie algebra. It is denoted

Lie⁡(G)=g.

The countable-choice assumption is used exactly through the supplied invariant-field and smooth-vector-field results.

Facts & Assumptions

Given: ACω and an n-dimensional real Lie group G with identity e.

[F1]

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

[F2]

A Lie group here is a finite-dimensional real smooth manifold. Lie group.

[F3]

The tangent space of an n-manifold is an n-dimensional real vector space. The tangent space of an n-manifold has dimension n.

[F4]

The tangent bracket is [u,v]G=[uL,vL]e, and [uL,vL]=[u,v]GL. Lie bracket on the tangent space of a Lie group.

[F5]

A finite-dimensional Lie algebra has a bilinear alternating bracket satisfying Jacobi. Finite-dimensional Lie algebra.

[F6]

Evaluation at e is a linear isomorphism from left-invariant smooth fields to TeG. Left-invariant vector fields evaluate isomorphically at the identity.

[F7]

Smooth vector fields have a bilinear alternating bracket satisfying Jacobi. Smooth vector fields form a Lie algebra under the Lie bracket.

Proof

technique · direct
1.1F2F3

By [F2] and [F3], g=TeG is an n-dimensional real vector space and hence is finite-dimensional.

1.2F4F6F7algebra

Because the inverse of the linear isomorphism in [F6] is linear, (au+bv)L=auL+bvL. Bilinearity of the field bracket in [F7] and the definition [F4] therefore give [au+bv,w]G=a[u,w]G+b[v,w]G, and similarly in the second variable.

1.3F4F7

Alternation of the field bracket in [F7] gives [u,u]G=[uL,uL]e=0. Thus the tangent bracket is alternating.

1.4F4F7

By [F4], the left-invariant extension of [v,w]G is [vL,wL]. Consequently the tangent Jacobi expression is the value at e of [uL,[vL,wL]]+[vL,[wL,uL]]+[wL,[uL,vL]], which vanishes by the vector-field Jacobi identity in [F7].

2.1F1F2F3F4F5F6F7step 1.1step 1.2step 1.3step 1.4∎

Steps 1.1--1.4 verify every axiom in [F5], so g is a finite-dimensional real Lie algebra. A Lie group is nonempty. If n=0, then g=0 and the bracket is the unique zero bracket; if n=1, alternation forces the bracket to vanish, consistently with the proof. No metric or nondegeneracy condition occurs, and the group is boundaryless by convention. The stated ACω is inherited through [F4], [F6], and the smooth-field meaning in [F7]; all algebraic transport is deterministic and adds no choice. The theorem verifies a structure rather than an iff.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Right-invariant fields carry the opposite Lie bracket

Statement

Assume ACω. For X,Y∈g=TeG, let XR,YR be their ordinary right-invariant smooth extensions, and let [X,Y]G be the tangent bracket defined through left-invariant fields. Then

[XR,YR]=−[X,Y]GR.

Thus evaluation identifies ordinary right-invariant fields with the opposite Lie algebra gop, not with the left-invariant bracket. The countable-choice assumption is used exactly through the supplied invariant-extension and tangent-bracket results.

Facts & Assumptions

Given: ACω, a Lie group G with inversion inv⁡(g)=g−1, and X,Y∈g=TeG.

[F1]

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

[F2]

Multiplication and inversion are smooth, and inversion is involutive. Lie group.

[F3]

Left- and ordinary right-invariant fields use Lg(h)=gh and Rg(h)=hg. Left- and right-invariant vector fields.

[F4]

Left and right invariant extensions exist uniquely and satisfy ZgL=d(Lg)eZ and ZgR=d(Rg)eZ. Left-invariant vector fields evaluate isomorphically at the identity.

[F5]

The tangent bracket satisfies [XL,YL]=[X,Y]GL. Lie bracket on the tangent space of a Lie group.

[F6]

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

[F7]

Tangent spaces of products split canonically as direct sums. Canonical tangent and cotangent splittings for products.

[F8]

The differential is defined by pullback of germs, and is a linear map. The differential of a smooth map, The differential sends derivations to derivations and is linear.

[F9]

Diffeomorphism pushforward preserves vector-field brackets. Diffeomorphism pushforward preserves Lie brackets.

[F10]

The field bracket is the commutator [U,V]f=U(Vf)−V(Uf). The Lie bracket of smooth vector fields.

Proof

technique · direct
1.1F2F6F7F8algebra

Let m:G×G→G be multiplication and let j1(g)=(g,e), j2(g)=(e,g). Under [F7], d(j1)e(A)=(A,0) and d(j2)e(B)=(0,B). Since m∘j1=m∘j2=id⁡G, the chain rule [F6] and linearity [F8] give dm(e,e)(A,B)=A+B.

2.1F2F6F8step 1.1algebra

The map g↦m(g,inv⁡(g)) is constant at e. By [F8], its differential annihilates every tangent vector because derivations annihilate constant germs. Applying [F6] and step 1.1 gives 0=dm(e,e)(Z,d(inv⁡)eZ)=Z+d(inv⁡)eZ. Hence d(inv⁡)e=−id⁡g.

3.1F3F4F6step 2.1

For h∈G, the identity inv⁡∘Lh=Rh−1∘inv⁡ and [F6] give d(inv⁡)h d(Lh)eZ=d(Rh−1)e d(inv⁡)eZ=−d(Rh−1)eZ. By [F4], as h varies this says inv⁡∗(ZL)=(−Z)R=−ZR.

4.1F5F9F10step 3.1algebra

Inversion is a diffeomorphism by [F2]. Apply [F9], step 3.1, and [F5]: [XR,YR]=[−XR,−YR]=[inv⁡∗XL,inv⁡∗YL]=inv⁡∗[XL,YL]=inv⁡∗([X,Y]GL)=−[X,Y]GR. The first equality uses the bilinearity visible directly in the commutator formula [F10].

5.1F1F2F3F4F5F6F7F8F9F10step 1.1step 2.1step 3.1step 4.1∎

A Lie group is nonempty. If dim⁡G=0, all fields and brackets vanish; in dimension one the tangent bracket vanishes by alternation, so the displayed identity again reads zero equals zero. No metric or nondegeneracy condition occurs, and the group is boundaryless by convention. The stated ACω is inherited through [F3], [F4], and [F5]; the product differential, inversion, and bracket calculation are canonical and add no choice. The proposition is a one-way sign identity, not a biconditional.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Left Maurer--Cartan form

Definition

Assume ACω as in The Axiom of Countable Choice (ACω), let G be a Lie group Lie group with identity e, and write g=TeG. A g-valued one-form on G means a smooth map α:TG→g whose restriction αg:TgG→g is linear for every g. Equivalently, V↦(πG(V),α(V)) is a smooth vector-bundle map TG→G×g over id⁡G in the sense of Vector bundle maps over a smooth base map.

The left Maurer--Cartan form is the g-valued one-form θ:TG→g whose fibre map at g is

θg=d(Lg−1)g:TgG⟶TeG=g.

This formula is well-defined because left translation by g−1 sends g to e. It is smooth and fibrewise linear because Translations are diffeomorphisms and their differentials trivialize the tangent bundle identifies

TG⟶G×g,Vg⟼(g,θgVg)

as the inverse vector-bundle isomorphism to left trivialization. In particular, θe=d(Le)e=id⁡g.

The stated ACω is used exactly through that supplied smooth left-trivialization theorem; the pointwise formula and passage to its second component add no choice. A Lie group is nonempty. When dim⁡G=0, θ is the unique map between zero tangent fibres, and the definition is unchanged in dimension one. Lie groups are boundaryless by convention, and no metric, nondegeneracy, endpoint, or biconditional occurs.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Maurer--Cartan form is a pointwise isomorphism and left invariant

Statement

Assume ACω. Let θ be the left Maurer--Cartan form of a Lie group G. Every fibre map θg:TgG→g is a linear isomorphism, with inverse d(Lg)e. For h,g∈G and V∈TgG, define the pullback here by

(Lh∗θ)g(V)=θhg(d(Lh)gV).

Then Lh∗θ=θ for every h∈G. Moreover, for every X∈g and its left-invariant extension XL,

θg(XgL)=X

at every g∈G. The countable-choice assumption is used exactly through the supplied Maurer--Cartan definition and invariant-extension theorem.

Facts & Assumptions

Given: ACω, a Lie group G with identity e, elements g,h∈G, a vector V∈TgG, and X∈g=TeG.

[F1]

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

[F2]

The left Maurer--Cartan form is θg=d(Lg−1)g, and its associated bundle map is the inverse of smooth left trivialization. Left Maurer--Cartan form.

[F3]

Left translations are La(b)=ab, with inverse La−1. Left and right translations on a Lie group.

[F4]

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

[F5]

The left-invariant extension of X∈g is XgL=d(Lg)eX. Left-invariant vector fields evaluate isomorphically at the identity.

Proof

technique · direct
1.1F2algebra

By [F2], the bundle map Vg↦(g,θgVg) is inverse to ΦL(g,X)=d(Lg)eX. Consequently each θg is a linear isomorphism with inverse d(Lg)e.

1.2F2F3F4algebra

The group law in [F3] gives L(hg)−1∘Lh=Lg−1. Therefore [F2] and the chain rule [F4] give (Lh∗θ)g(V)=d(L(hg)−1)hg d(Lh)gV=d(Lg−1)gV=θg(V). Since g and V were arbitrary, Lh∗θ=θ.

2.1F2F5step 1.1

By [F5], [F2], and step 1.1, θg(XgL)=θg(d(Lg)eX)=X. Thus the g-valued function θ(XL) is the constant function with value X.

3.1F1F2F3F4F5step 1.1step 1.2step 2.1∎

A Lie group is nonempty. In dimension zero all tangent spaces are zero and the unique fibre maps give every asserted identity; in dimension one the same proof applies. Lie groups are boundaryless by convention, and no metric, nondegeneracy, or endpoint occurs. The stated ACω is inherited through [F2] and [F5]; the chain-rule identities are pointwise and add no selection. The proposition asserts equalities and an explicit inverse, not a biconditional.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Finite-dimensional vector-valued forms and their exterior derivative

Definition

Let M be a smooth manifold, let V be a finite-dimensional real vector space, and let k≥0. A smooth V-valued differential k-form on M is a family of alternating k-linear maps

αp:(TpM)k⟶V

such that λ∘α is a scalar smooth k-form in the sense of A smooth differential k-form for every λ∈V∗. Equivalently, for one (and hence every) basis (v1,…,vr) of V, the unique components in α=∑iviαi all belong to Ωk(M).

For such an α, its componentwise exterior derivative is the unique V-valued (k+1)-form dVα characterized by

λ∘dVα=d(λ∘α)

for every λ∈V∗. Indeed, in a basis with dual basis (λ1,…,λr), set

dVα=∑ivi dαi,αi=λi∘α.

The scalar formula defining d is real-linear term by term The exterior derivative by the invariant vector-field formula, and its output is a smooth form The invariant exterior-derivative formula is C∞-multilinear. Thus the displayed construction has the stated characterization. It is independent of the chosen basis because linear functionals separate points of V, and the characterization also proves uniqueness.

The two smoothness descriptions are equivalent in both directions: testing all λ includes the dual basis components, while every λ∘α is a fixed real linear combination of the components in one basis. If M is empty, these assignments and identities are vacuous. If V=0, there is only the zero-valued form and its derivative is zero; if dim⁡V=1, the definition is exactly the scalar definition after choosing one nonzero basis vector. No metric, nondegeneracy, manifold boundary, or endpoint is involved. A single finite basis exists by finite-dimensionality; the definition is basis-independent and chooses no basis or family, so no choice axiom is used.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Maurer--Cartan structure equation

Statement

Assume ACω. Let θ be the left Maurer--Cartan form of a Lie group G, with values in g=TeG. Write dθ for its componentwise exterior derivative from Finite-dimensional vector-valued forms and their exterior derivative. For vector fields A,B, define the bracket-valued wedge by

[θ∧θ](A,B)=[θ(A),θ(B)]G−[θ(B),θ(A)]G=2[θ(A),θ(B)]G.

Then the normalized left Maurer--Cartan structure equation is

dθ+12[θ∧θ]=0.

The countable-choice assumption is used exactly through the supplied Maurer--Cartan, invariant-field, and tangent-bracket results.

Facts & Assumptions

Given: ACω, a Lie group G with identity e, its left Maurer--Cartan form θ, and g=TeG with the transported left-invariant-field bracket.

[F1]

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

[F2]

Finite-dimensional vector-valued forms and their componentwise exterior derivative are defined by scalar dual evaluation. Finite-dimensional vector-valued forms and their exterior derivative.

[F3]

Every θp is a linear isomorphism with inverse d(Lp)e, and θ(XL)=X. Maurer--Cartan form is a pointwise isomorphism and left invariant.

[F4]

The transported tangent bracket satisfies [XL,YL]=[X,Y]GL. Lie bracket on the tangent space of a Lie group.

[F5]

The tangent bracket is bilinear and alternating. The tangent space at the identity is a Lie algebra.

[F6]

Every X∈g has a unique smooth left-invariant extension. Left-invariant vector fields evaluate isomorphically at the identity.

[F7]

For a scalar one-form α, dα(A,B)=A(α(B))−B(α(A))−α([A,B]). The exterior derivative by the invariant vector-field formula.

Proof

technique · direct
1.1F3F5algebra

Bilinearity of the bracket [F5] and smoothness of θ [F3] show in any basis of g that the displayed bracket-wedge has smooth components; alternation follows by exchanging A and B. Thus it is a well-defined g-valued two-form. Because the bracket is alternating, [F5] also gives [θ∧θ](A,B)=2[θ(A),θ(B)]G.

1.2F2F3F4F6F7algebra

Let X,Y∈g and use their left-invariant extensions from [F6]. For every λ∈g∗, [F2], [F7], and [F3] give λ(dθ(XL,YL))=XL(λ(θ(YL)))−YL(λ(θ(XL)))−λ(θ([XL,YL]))=−λ([X,Y]G), because the first two functions are the constants λ(Y) and λ(X) and [F4] identifies the bracket field. Since linear functionals separate points, dθ(XL,YL)=−[X,Y]G.

2.1F3step 1.1step 1.2algebra

On the same fields, step 1.1 and [F3] yield 12[θ∧θ](XL,YL)=[X,Y]G. Adding this to step 1.2 proves the structure equation on every pair of left-invariant fields.

3.1F3F6step 2.1

Fix p∈G and U,V∈TpG. Put X=θp(U) and Y=θp(V). By [F3], θp(XpL)=X=θp(U) and θp(YpL)=Y=θp(V); injectivity of θp gives XpL=U and YpL=V. Step 2.1 therefore makes the structure equation vanish on the arbitrary pair (U,V) at p, proving it globally.

4.1F1F2F3F4F5F6F7step 1.1step 1.2step 2.1step 3.1∎

A Lie group is nonempty. If dim⁡G=0, both two-forms are uniquely zero; if dim⁡G=1, every alternating two-form is zero and the equation again holds. Lie groups are boundaryless by convention, and no metric, nondegeneracy, or endpoint is involved. The stated ACω is inherited through [F3], [F4], [F5], and [F6]; componentwise differentiation and the pointwise spanning argument add no choice. The theorem is one equality, not a biconditional.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

One-parameter subgroup of a Lie group

Definition

The standard coordinate on R makes addition (s,t)↦s+t and inversion t↦−t smooth, so (R,+) is a one-dimensional Lie group in the sense of Lie group. A one-parameter subgroup of a Lie group G is a Lie-group homomorphism

γ:(R,+)⟶G

in the sense of Lie-group homomorphism, isomorphism, and automorphism. Thus γ is smooth, is defined for every real parameter, and satisfies

γ(s+t)=γ(s)γ(t),γ(0)=e,γ(−t)=γ(t)−1.

The last two identities are consequences of the group-homomorphism law, not extra data. A smooth curve defined only on an interval around 0 is therefore not yet a one-parameter subgroup, even if it satisfies the product law whenever all displayed parameters remain in that interval. The term also does not assert that the image is embedded or closed.

Both the domain and every Lie-group codomain are nonempty and boundaryless. For a zero-dimensional codomain the definition still permits, for example, the constant homomorphism; for a one-dimensional codomain it is unchanged. No metric, nondegeneracy, or finite endpoint occurs, and all maps and group operations are supplied explicitly, so no choice axiom is used. This is a definition, not a biconditional characterization.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Left-invariant vector fields are complete

Statement

Assume ACω. Every left-invariant smooth vector field on a finite-dimensional real Lie group is complete. Equivalently, its maximal flow is defined on all of R×G. The countable-choice assumption is used exactly through the supplied invariant-field and smooth-tangent-bundle framework.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with identity e, and a left-invariant smooth vector field X on G.

[F1]

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

[F2]

Left invariance means d(La)q(Xq)=Xaq for all a,q∈G. Left- and right-invariant vector fields.

[F3]

Through every point there is a unique maximal integral curve on an open interval containing zero. Through each point there is a unique maximal integral curve.

[F4]

An integral curve c satisfies c′(t)=Xc(t). Integral curves of a vector field.

[F5]

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

[F6]

Completeness means that every maximal integral curve has domain all of R. Complete vector fields.

[F7]

A vector field is complete if and only if its maximal flow domain is all of R×G. A vector field is complete if and only if its flow is global.

Proof

technique · direct
1.1F3choose

Let c:I→G be the maximal integral curve of X with c(0)=e, supplied by [F3]. Since I is open and contains 0, fix δ>0 with (−δ,δ)⊆I.

2.1F2F3F4F5step 1.1

For s∈I, define ηs(t)=c(s)c(t−s) on (s−δ,s+δ). By [F4], [F5], and left invariance [F2], ηs′(t)=d(Lc(s))c(t−s)c′(t−s)=d(Lc(s))c(t−s)Xc(t−s)=Xηs(t). Also ηs(s)=c(s)c(0)=c(s). After shifting the parameter by s, uniqueness in [F3] shows that ηs and c agree wherever their domains overlap near s, and hence on their whole interval overlap by the same local uniqueness argument.

3.1F3step 1.1step 2.1constructcontradiction

Suppose the right endpoint b=sup⁡I were finite. Choose s∈I with b−δ/2<s<b. Then s+δ>b, while step 2.1 makes c and ηs agree on the nonempty overlap. Splicing them therefore gives an integral curve through e on the strictly larger interval I∪(s−δ,s+δ), contradicting maximality in [F3]. The identical argument at the left endpoint, using s with a<s<a+δ/2 if a=inf⁡I were finite, excludes a finite left endpoint. Thus I=R.

4.1F2F3F4F5F6step 2.1step 3.1

For an arbitrary p∈G, define cp(t)=pc(t) on all of R. The calculation of step 2.1 with c(s) replaced by the fixed element p proves that cp is an integral curve of X, and cp(0)=p. Its domain is already all of R, so maximal uniqueness [F3] and [F6] show that X is complete.

5.1F7step 4.1

By [F7], completeness is equivalent to the maximal flow domain being all of R×G, which proves the final formulation in the statement.

6.1F1F2F3F4F5F6F7step 1.1step 2.1step 3.1step 4.1step 5.1∎

A Lie group is nonempty. In dimension zero every smooth vector field is zero and its integral curves are constant; in dimension one the extension proof above is unchanged. Lie groups are boundaryless, so no boundary or finite-time endpoint exception remains, and no metric or nondegeneracy enters. The stated ACω is inherited through [F2] and the smooth tangent-field framework; choosing one δ and one s inside a single nonempty interval uses no family choice, and the endpoint argument adds no choice. The theorem is a direct assertion plus the supplied equivalence in [F7]; both directions of that cited equivalence are available.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

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

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g=TeG.

If γ:R→G is a one-parameter subgroup and X=γ′(0), then

γ′(t)=d(Lγ(t))eX=Xγ(t)L

for every t∈R; thus γ is the integral curve through e of the left-invariant field XL. Conversely, the global integral curve through e of XL is a one-parameter subgroup. Consequently every X∈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: ACω, a finite-dimensional real Lie group G with identity e, and X∈g=TeG.

[F1]

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

[F2]

A one-parameter subgroup is a smooth homomorphism γ:(R,+)→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 XgL=d(Lg)eX. This result assumes ACω through the smooth tangent-bundle framework. Left-invariant vector fields evaluate isomorphically at the identity.

[F4]

Every left-invariant smooth field is complete, assuming ACω 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)=Yc(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.1F2F3F5F7algebra

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))eX=Xγ(t)L. Hence γ is an integral curve of XL through e.

1.2F3F4F6construct

Conversely, let XL be the unique field supplied by [F3]. By [F4] and [F6], its maximal integral curve c:R→G with c(0)=e is global. Fix s∈R and define as(t)=c(s+t) and bs(t)=c(s)c(t). Both curves are defined for every real t, and as(0)=bs(0)=c(s).

2.1F3F5F6F7step 1.2algebra

By [F5], as′(t)=Xc(s+t)L=Xas(t)L. The chain rule and left invariance give bs′(t)=d(Lc(s))c(t)c′(t)=d(Lc(s))c(t)Xc(t)L=Xc(s)c(t)L=Xbs(t)L. Thus as and bs 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∈R.

3.1F2F3F5F6step 1.1step 2.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)=XeL=X. If γ is any other one-parameter subgroup with initial velocity X, step 1.1 makes it an integral curve of XL through e, and [F6] forces γ=c. This proves existence and uniqueness for every X∈g.

4.1F1F2F3F4F5F6F7step 1.1step 1.2step 2.1step 3.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 ACω, 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.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Exponential map of a Lie group

Definition

Assume ACω, let G be a finite-dimensional real Lie group with identity e, and write g=TeG. For each X∈g, the existence-and-uniqueness theorem One-parameter subgroups are integral curves of left-invariant fields supplies a unique one-parameter subgroup γX:R→G with γX′(0)=X. The exponential map of G is the well-defined total map

exp⁡G:g⟶G,exp⁡G(X):=γX(1).

Here ACω is the axiom of countable choice. The same theorem identifies γX with the integral curve through e of the left-invariant field XL; the left translate t↦gγX(t) is therefore the corresponding integral curve through g. The countable-choice assumption is used exactly through that supplied smooth invariant-field and completeness result, and evaluation at the single time 1 adds no choice.

A Lie group is nonempty and boundaryless. If dim⁡G=0, then g=0 and exp⁡G(0)=e; the definition is unchanged in dimension one. No metric or nondegeneracy condition occurs, and 1 is not an endpoint of the global parameter domain R. This item defines a map and asserts no biconditional characterization.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Exponential scales one-parameter subgroups

Statement

Assume ACω. Let G be a finite-dimensional real Lie group, let g=TeG, and let γX denote the unique one-parameter subgroup with initial velocity X∈g. Then, for every a∈R,

γX(a)=exp⁡G(aX).

Consequently, for all s,t∈R,

exp⁡G((s+t)X)=exp⁡G(sX)exp⁡G(tX).

The countable-choice assumption is used exactly through the supplied existence-and-uniqueness theorem for one-parameter subgroups.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with identity e, its Lie algebra g=TeG, a vector X∈g, and real numbers a,s,t.

[F1]

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

[F2]

The exponential map is defined by exp⁡G(Y)=γY(1), where γY is the unique one-parameter subgroup with initial velocity Y. Exponential map of a Lie group.

[F3]

Assuming ACω, every Y∈g determines a unique one-parameter subgroup γY with γY′(0)=Y. One-parameter subgroups are integral curves of left-invariant fields.

[F4]

A one-parameter subgroup γ is smooth and satisfies γ(u+v)=γ(u)γ(v) for all u,v∈R. One-parameter subgroup of a Lie group.

[F5]

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

Proof

technique · direct
1.1F3F4F5algebra

Fix a∈R and define δa(u)=γX(au). By [F4], δa(u+v)=γX(a(u+v))=γX(au)γX(av)=δa(u)δa(v), so δa is a one-parameter subgroup. By [F5], its initial velocity is δa′(0)=aγX′(0)=aX.

2.1F2F3step 1.1

Both δa and γaX are one-parameter subgroups with initial velocity aX. Uniqueness in [F3] therefore gives δa=γaX. Evaluating at u=1 and applying [F2], γX(a)=δa(1)=γaX(1)=exp⁡G(aX).

3.1F4step 2.1algebra

For s,t∈R, [F4] and step 2.1 give exp⁡G((s+t)X)=γX(s+t)=γX(s)γX(t)=exp⁡G(sX)exp⁡G(tX).

4.1F1F2F3F4F5step 1.1step 2.1step 3.1∎

Lie groups are nonempty and boundaryless. If dim⁡G=0, then X=0 and all displayed curves are constant; in dimension one the proof is unchanged. Every curve has domain R, so a,s,t may be zero, negative, or any finite values without an endpoint issue. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F2] and [F3]; fixing finitely many vectors and scalars adds no choice. The result consists of two identities, not a biconditional.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The Lie-group exponential map is smooth with identity differential at zero

Statement

Assume ACω. For a finite-dimensional real Lie group G, the exponential map

exp⁡G:g=TeG⟶G

is smooth, satisfies exp⁡G(0)=e, and, under the canonical identification T0g≃g, has differential

d(exp⁡G)0=id⁡g.

The countable-choice assumption is used exactly through the supplied smooth tangent-bundle trivialization and one-parameter-subgroup results.

Facts & Assumptions

Given: ACω and a finite-dimensional real Lie group G with identity e and Lie algebra g=TeG.

[F1]

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

[F2]

The exponential map is the total map exp⁡G(Y)=γY(1). Exponential map of a Lie group.

[F3]

Assuming ACω, the map (g,Y)↦d(Lg)eY is a smooth vector-bundle trivialization G×g→TG. Translations are diffeomorphisms and their differentials trivialize the tangent bundle.

[F4]

Assuming ACω, every Y∈g determines a unique global one-parameter subgroup γY, and γY′(t)=d(LγY(t))eY. One-parameter subgroups are integral curves of left-invariant fields.

[F5]

The maximal flow of a smooth vector field has open domain, is smooth on that domain, and is uniquely determined by its maximal integral curves. The fundamental theorem on flows.

[F6]

The scaling identity is γY(a)=exp⁡G(aY) for all a∈R. Exponential scales one-parameter subgroups.

[F7]

Every one-parameter subgroup satisfies γ(0)=e. One-parameter subgroup of a Lie group.

[F8]

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

Proof

technique · direct
1.1F3construct

On the product manifold M=G×g, define X(g,Y):=(d(Lg)eY,0)∈TgG×TYg=T(g,Y)M. Its first component is the smooth map supplied by [F3], and its second component is the zero field on the vector space g. Hence X is a smooth vector field on M.

2.1F3F4F5F8step 1.1algebra

For (g,Y)∈M, define cg,Y:R→M by cg,Y(t)=(gγY(t),Y). By [F4], [F8], and Lg∘LγY(t)=LgγY(t), cg,Y′(t)=(d(Lg)γY(t)d(LγY(t))eY,0)=(d(LgγY(t))eY,0)=Xcg,Y(t). Thus cg,Y is an integral curve of X through (g,Y) and is defined on all of R. Every maximal integral curve of X is therefore global. By [F5], the global flow is smooth and is Ψ(t,(g,Y))=(gγY(t),Y).

3.1F2F5step 2.1

Restricting this smooth flow to (t,(e,Y)) and projecting to G shows that (t,Y)↦γY(t) is smooth. Restricting further to t=1 gives the map Y↦γY(1)=exp⁡G(Y), which is smooth by [F2].

4.1F4F6F7F8step 3.1algebra

By [F6] with a=0 and [F7], exp⁡G(0)=γX(0)=e. Fix X∈g and consider qX(a)=aX. Applying [F8] to exp⁡G∘qX and then [F6] gives d(exp⁡G)0(X)=dda∣a=0exp⁡G(aX)=dda∣a=0γX(a)=γX′(0)=X. Hence d(exp⁡G)0 is the identity under T0g≃g.

5.1F1F2F3F4F5F6F7F8step 1.1step 2.1step 3.1step 4.1∎

Lie groups are nonempty and boundaryless. If dim⁡G=0, then g=0, the exponential maps the unique vector to e, and its differential is the identity of the zero space; in dimension one the proof is unchanged. The global curves in step 2.1 remove finite-time endpoint issues. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F2]--[F4] and especially the smooth tangent-bundle trivialization [F3]; forming one product field and restricting its flow adds no choice. No biconditional is asserted.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The exponential map is a local diffeomorphism at zero

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with identity e and Lie algebra g. There are open neighborhoods V⊆g of 0 and U⊆G of e such that

exp⁡G∣V:V⟶U

is a diffeomorphism. The countable-choice assumption is inherited exactly from the supplied smoothness and identity-differential theorem.

Facts & Assumptions

Given: ACω and a finite-dimensional real Lie group G with identity e and Lie algebra g.

[F1]

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

[F2]

Assuming ACω, exp⁡G is smooth, exp⁡G(0)=e, and d(exp⁡G)0=id⁡g. The Lie-group exponential map is smooth with identity differential at zero.

[F3]

A smooth map whose differential at a point is an isomorphism restricts to a diffeomorphism between neighborhoods of that point and its image. The smooth inverse function theorem on manifolds.

Proof

technique · direct
1.1F2

By [F2], exp⁡G is smooth, sends 0 to e, and its differential at 0 is the identity of g, hence a linear isomorphism.

2.1F2F3step 1.1

Apply [F3] to F=exp⁡G at 0. Using step 1.1, obtain open neighborhoods V of 0 and U of e=exp⁡G(0) such that exp⁡G∣V:V→U is a diffeomorphism.

3.1F1F2F3step 1.1step 2.1∎

Lie groups are nonempty and boundaryless. If dim⁡G=0, then V={0} and U={e} may be chosen open and the restriction is the unique diffeomorphism; in dimension one the same inverse function theorem applies. The neighborhoods are open and contain their named points, so there is no endpoint issue. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F2]; applying [F3] once adds no family choice. No biconditional is asserted.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Local logarithm on a Lie group

Definition

Assume ACω, let G be a finite-dimensional real Lie group with identity e, and write g=TeG. Fix open neighborhoods V⊆g of 0 and U⊆G of e for which

exp⁡G∣V:V⟶U

is the diffeomorphism supplied by The exponential map is a local diffeomorphism at zero. The local logarithm associated with (V,U) is its smooth inverse

log⁡G:U⟶V.

Thus log⁡G(exp⁡GX)=X for X∈V and exp⁡G(log⁡Gg)=g for g∈U. The neighborhoods are part of the notation: no value of log⁡G is asserted outside U, and no global logarithm is claimed.

Here ACω is countable choice. It is inherited exactly through the local-diffeomorphism supplier. Fixing one witness pair (V,U) by existential instantiation is not a choice from a family and adds no choice principle.

The neighborhood U contains e and is nonempty. If dim⁡G=0, one may take V={0} and U={e} and the logarithm is the unique inverse; the definition is unchanged in dimension one. Open neighborhoods rather than closed intervals are involved, so there is no endpoint case. No metric or nondegeneracy condition occurs. The two inverse identities unpack the phrase "inverse map" and do not assert a biconditional characterization.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

One-parameter subgroups are exactly exponentials

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. A smooth curve γ:R→G is a one-parameter subgroup if and only if there is a unique X∈g such that

γ(t)=exp⁡G(tX)

for every t∈R. Necessarily X=γ′(0). The countable-choice assumption is used exactly through the supplied existence and uniqueness of the one-parameter subgroups γX.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with Lie algebra g, and a smooth curve γ:R→G.

[F1]

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

[F2]

The scaling identity is γX(t)=exp⁡G(tX). Exponential scales one-parameter subgroups.

[F3]

A one-parameter subgroup is a smooth homomorphism (R,+)→G. One-parameter subgroup of a Lie group.

[F4]

Assuming ACω, every X∈g determines a unique one-parameter subgroup γX with γX′(0)=X, and any one-parameter subgroup having initial velocity X is this curve. One-parameter subgroups are integral curves of left-invariant fields.

Proof

technique · direct
1.1F2F3F4algebra

Suppose γ is a one-parameter subgroup, and put X=γ′(0). By uniqueness in [F4], γ=γX, so [F2] gives γ(t)=exp⁡G(tX) for every real t. If also γ(t)=exp⁡G(tY) for every t, [F2] identifies this curve with γY; differentiating at zero yields Y=γ′(0)=X.

1.2F2F3F4

Conversely, fix X∈g. By [F4], γX is a one-parameter subgroup, and [F2] gives t↦exp⁡G(tX)=γX(t). Hence every exponential curve is a one-parameter subgroup in the sense of [F3].

2.1F1F2F3F4step 1.1step 1.2∎

Lie groups are nonempty and boundaryless. If dim⁡G=0, then X=0 and the only exponential curve is constant; in dimension one the proof is unchanged. The curves have domain all of R, so there is no finite endpoint. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F2] and [F4]; taking one derivative adds no choice. Step 1.1 proves the forward implication and uniqueness, and step 1.2 proves the reverse implication.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-09-14Open item page →

Commuting Lie-algebra elements have multiplicative exponentials

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. If X,Y∈g satisfy [X,Y]G=0, then

exp⁡G(X+Y)=exp⁡G(X)exp⁡G(Y)=exp⁡G(Y)exp⁡G(X).

The countable-choice assumption is used exactly through the supplied tangent bracket, invariant-field, and exponential results.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with identity e and Lie algebra g, and X,Y∈g with [X,Y]G=0.

[F1]

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

[F2]

Lie-group multiplication m:G×G→G is smooth. Lie group.

[F3]

The tangent bracket satisfies [XL,YL]=[X,Y]GL. Lie bracket on the tangent space of a Lie group.

[F4]

Two smooth vector fields have commuting local flows if and only if their bracket vanishes. Two vector fields commute if and only if their local flows commute.

[F5]

The one-parameter subgroup γX is the global identity integral curve of XL. One-parameter subgroups are integral curves of left-invariant fields.

[F6]

The scaling and additive-parameter identities are γX(t)=exp⁡G(tX) and exp⁡G((s+t)X)=exp⁡G(sX)exp⁡G(tX). Exponential scales one-parameter subgroups.

[F7]

A one-parameter subgroup is a smooth homomorphism (R,+)→G. One-parameter subgroup of a Lie group.

[F8]

A one-parameter subgroup with initial velocity Z is exactly the curve t↦exp⁡G(tZ). One-parameter subgroups are exactly exponentials.

[F9]

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

Proof

technique · direct
1.1F3F4

By [F3], [XL,YL]=[X,Y]GL=0. The forward implication of [F4] therefore says that the global flows of XL and YL commute.

2.1F3F4F5F6F9step 1.1

By [F3], XL and YL are left invariant. For fixed g, the chain rule and left invariance show that the left translates of the identity integral curves in [F5] are integral curves through g. Hence [F5] and [F6] give the global flows ΦtX(g)=gexp⁡G(tX) and ΦsY(g)=gexp⁡G(sY). Evaluating the commutation identity from step 1.1 at e gives exp⁡G(sY)exp⁡G(tX)=exp⁡G(tX)exp⁡G(sY) for every s,t∈R.

3.1F2F6F7step 2.1algebra

Define c(t)=exp⁡G(tX)exp⁡G(tY). It is smooth by [F2], [F5], and [F6]. For s,t∈R, [F6] and step 2.1 give c(s+t)=exp⁡G(sX)exp⁡G(tX)exp⁡G(sY)exp⁡G(tY)=exp⁡G(sX)exp⁡G(sY)exp⁡G(tX)exp⁡G(tY)=c(s)c(t). Also c(0)=e, so c is a one-parameter subgroup by [F7].

4.1F2F5F6F9step 3.1algebra

Let m:G×G→G be multiplication and put α(t)=exp⁡G(tX) and β(t)=exp⁡G(tY). The identities m(g,e)=g and m(e,h)=h show that dm(e,e)(X,0)=X and dm(e,e)(0,Y)=Y. Since a differential is linear, dm(e,e)(X,Y)=X+Y. Hence [F5], [F6], and [F9] give c′(0)=X+Y.

5.1F7F8step 2.1step 3.1step 4.1

By [F8], the one-parameter subgroup c with initial velocity X+Y is c(t)=exp⁡G(t(X+Y)). At t=1, exp⁡G(X+Y)=exp⁡G(X)exp⁡G(Y). Step 2.1 with s=t=1 also gives exp⁡G(X)exp⁡G(Y)=exp⁡G(Y)exp⁡G(X).

6.1F1F2F3F4F5F6F7F8F9step 1.1step 2.1step 3.1step 4.1step 5.1∎

Lie groups are nonempty and boundaryless. If dim⁡G=0, then X=Y=0 and all terms equal e; in dimension one the proof is unchanged. All flows and exponential curves are global, so no endpoint issue occurs. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F3], [F5], [F6], and [F8]; fixing two fields and finitely many parameters adds no choice. No biconditional is asserted.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Lie-algebra homomorphism

Definition

Let g and h be finite-dimensional Lie algebras over the same field F∈{R,C}. A Lie-algebra homomorphism

φ:g⟶h

is an F-linear map, in the sense of Linear map between vector spaces over the same field, such that

φ([X,Y]g)=[φ(X),φ(Y)]h

for every X,Y∈g. Both linearity and bracket preservation are requirements. For complex Lie algebras, φ must therefore be complex-linear, not merely real-linear.

The zero brackets allowed by Finite-dimensional Lie algebra are not required to be nondegenerate. The unique linear map from the zero Lie algebra to any h is a homomorphism. One-dimensional Lie algebras have zero bracket, so a linear map between two such algebras preserves the bracket automatically, while a linear map from an abelian algebra to a nonabelian one still has to have commuting image.

The source and target are nonempty because they contain zero. The supplied map is data, and checking the two universal algebraic identities uses no choice. There is no metric, manifold boundary, interval, or endpoint. This is a definition with two simultaneous requirements, not a biconditional theorem.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Differential of a Lie-group homomorphism is a Lie-algebra homomorphism

Statement

Assume ACω. Let F:G→H be a homomorphism of finite-dimensional real Lie groups, with Lie algebras g=TeG and h=TeHH. Then

dFe:g⟶h

is a Lie-algebra homomorphism. The countable-choice assumption is used exactly through the supplied smooth invariant-field and tangent-bracket results.

Facts & Assumptions

Given: ACω, finite-dimensional real Lie groups G,H, and a Lie-group homomorphism F:G→H.

[F1]

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

[F2]

A Lie-algebra homomorphism is a linear map preserving brackets. Lie-algebra homomorphism.

[F3]

The map F is smooth, preserves identities, and satisfies F(gh)=F(g)F(h). Lie-group homomorphism, isomorphism, and automorphism.

[F4]

Pairs of related smooth vector fields have related brackets. Related vector fields have related Lie brackets.

[F5]

Assuming ACω, each tangent vector has a unique left-invariant smooth extension XgL=d(Lg)eX. Left-invariant vector fields evaluate isomorphically at the identity.

[F6]

The tangent bracket is characterized by [XL,YL]=[X,Y]gL, and similarly for h. Lie bracket on the tangent space of a Lie group.

[F7]

The differential of a smooth map at a point is linear. The differential sends derivations to derivations and is linear.

[F8]

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

Proof

technique · direct
1.1F3F5F8algebra

Fix X∈g. By [F5], X and dFeX have left-invariant extensions XL on G and (dFeX)L on H. For every g∈G, the homomorphism law [F3] gives F∘Lg=LF(g)∘F. Therefore [F8] gives dFg(XgL)=dFgd(Lg)eX=d(LF(g))eHdFeX=(dFeX)F(g)L. Thus XL and (dFeX)L are F-related.

2.1F4F5F6step 1.1

Apply [F4] to the related pairs from step 1.1 for X and Y. Then [XL,YL] is F-related to [(dFeX)L,(dFeY)L]. Evaluating relatedness at e and using [F6] on both groups yields dFe([X,Y]g)=[dFeX,dFeY]h.

3.1F2F6F7step 2.1

By [F7], dFe is linear, and step 2.1 proves bracket preservation. Hence dFe is a Lie-algebra homomorphism by [F2].

4.1F1F2F3F4F5F6F7F8step 1.1step 2.1step 3.1∎

Lie groups are nonempty and boundaryless. If either Lie algebra is zero-dimensional, the same related-field calculation applies and all relevant source vectors or target values are zero; in dimension one the proof is unchanged. No metric, nondegeneracy, interval, or endpoint occurs. The only choice use is the stated ACω, inherited through [F5] and [F6]; fixing two tangent vectors adds no choice. No biconditional is asserted.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Exponential map is natural for Lie-group homomorphisms

Statement

Assume ACω. If F:G→H is a homomorphism of finite-dimensional real Lie groups, then for every X∈g=TeG,

F(exp⁡GX)=exp⁡H(dFeX).

The countable-choice assumption is used exactly through the supplied one-parameter-subgroup/exponential characterization.

Facts & Assumptions

Given: ACω, a Lie-group homomorphism F:G→H, and X∈g=TeG.

[F1]

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

[F2]

A one-parameter subgroup with initial velocity Y is uniquely the curve t↦exp⁡(tY). One-parameter subgroups are exactly exponentials.

[F3]

The map F is smooth, preserves identities, and satisfies F(gh)=F(g)F(h). Lie-group homomorphism, isomorphism, and automorphism.

[F4]

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

Proof

technique · direct
1.1F2F3

By [F2], aX(t)=exp⁡G(tX) is a one-parameter subgroup. Since [F3] makes F a smooth group homomorphism, the composite c(t)=F(aX(t)) is a one-parameter subgroup of H.

2.1F2F3F4step 1.1

The same characterization [F2] gives aX′(0)=X. Hence the chain rule [F4] yields c′(0)=dFe(aX′(0))=dFeX.

3.1F2step 1.1step 2.1

Apply [F2] in H: the unique one-parameter subgroup with initial velocity dFeX is t↦exp⁡H(t dFeX). Steps 1.1--2.1 identify c with this curve. Evaluating at t=1 gives F(exp⁡GX)=exp⁡H(dFeX).

4.1F1F2F3F4step 1.1step 2.1step 3.1∎

Both Lie groups are nonempty and boundaryless. Zero-dimensional source or target Lie algebras and dimension one require no change, including X=0. The one-parameter curves are global, so no endpoint issue occurs. No metric or nondegeneracy condition occurs. The only choice use is the stated ACω, inherited through [F2]; composition with one supplied homomorphism and evaluation at one add no choice. No biconditional is asserted.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A homomorphism from a connected Lie group is determined by its differential at the identity

Statement

Assume ACω. Let G and H be finite-dimensional real Lie groups, with G connected. If two Lie-group homomorphisms F1,F2:G→H satisfy

d(F1)e=d(F2)e:TeG⟶TeH,

then F1=F2. The countable-choice assumption is inherited exactly from the supplied exponential-map results.

Facts & Assumptions

Given: ACω, finite-dimensional real Lie groups G,H with G connected, and Lie-group homomorphisms F1,F2:G→H with equal differentials at the identity e∈G.

[F1]

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

[F2]

A Lie-group homomorphism intertwines exponential maps: F(exp⁡GX)=exp⁡H(dFeX). Exponential map is natural for Lie-group homomorphisms.

[F3]

There are open neighborhoods V⊆TeG of 0 and U⊆G of e such that exp⁡G∣V:V→U is a diffeomorphism. The exponential map is a local diffeomorphism at zero.

[F4]

A Lie-group homomorphism is smooth, preserves products, identities, and inverses. Lie-group homomorphism, isomorphism, and automorphism.

[F5]

A connected topological space has no partition into two nonempty clopen subsets. Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets.

Proof

technique · direct
1.1F2F3

Fix the neighborhoods V,U supplied by [F3]. If g∈U, then g=exp⁡GX for a unique X∈V. By [F2] and the hypothesis on the differentials, F1(g)=exp⁡H(d(F1)eX)=exp⁡H(d(F2)eX)=F2(g). Thus F1 and F2 agree on the open identity neighborhood U.

2.1F4step 1.1

Let K={g∈G:F1(g)=F2(g)}. The identity belongs to K. If g,h∈K, then [F4] gives F1(gh)=F1(g)F1(h)=F2(g)F2(h)=F2(gh), and similarly F1(g−1)=F1(g)−1=F2(g)−1=F2(g−1). Hence K is a subgroup of G, and step 1.1 gives U⊆K.

3.1F4step 2.1

For each k∈K, the translate kU is open and is contained in K; conversely every k∈K belongs to kU because e∈U. Therefore K=⋃k∈KkU is open. Every left coset gK is then open as well. If g∉K, the coset gK is disjoint from K: an element x∈gK∩K would imply g=xk−1∈K. Hence G∖K=⋃g∉KgK is open, so K is also closed.

4.1F5step 2.1step 3.1

The set K is nonempty because it contains e. If its complement were nonempty, step 3.1 would partition G into the two nonempty clopen sets K and G∖K, contradicting connectedness by [F5]. Thus K=G, which means F1=F2.

5.1F1F2F3F4F5step 1.1step 2.1step 3.1step 4.1∎

Lie groups are nonempty and boundaryless. In dimension zero a connected Lie group is a one-point discrete space, so the conclusion also follows directly; dimension one requires no change. There is no metric, degeneracy, or endpoint issue. The only choice use is the stated ACω inherited through [F2] and [F3]. Fixing one supplied neighborhood pair and forming unions over already specified sets select no family of witnesses. No biconditional is asserted.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passaudited 2026-09-14Open item page →

Conjugation and the adjoint representation of a Lie group

Definition

Let G be a finite-dimensional real Lie group with identity e and Lie algebra g=TeG. For g∈G, conjugation by g is

Cg:G⟶G,Cg(h)=ghg−1.

It is a Lie-group automorphism. Indeed, associativity gives Cg(hk)=Cg(h)Cg(k), its smoothness follows from the smooth multiplication and inversion of Lie group, and Cg−1 is its smooth inverse. Thus its differential at the identity is the invertible linear map

Ad⁡g:=d(Cg)e:g⟶g.

Here Cg(e)=e, so the source and target tangent spaces are both g; invertibility follows from The differential of a diffeomorphism is an isomorphism. Write GL⁡(g) for the group of invertible real-linear maps of g in the sense of Invertible linear maps, linear isomorphisms, and inverse linear maps. The adjoint map is

Ad⁡:G⟶GL⁡(g),g⟼Ad⁡g.

The target carries its standard smooth structure. Explicitly, if n=dim⁡g≥1, one fixed basis identifies L(g,g) with Mn(R)≃Rn2 by Coordinate columns [v]B and matrices [T]BC of linear maps relative to ordered bases. Under this identification GL⁡(g) is the open set det⁡≠0: determinant is a polynomial by For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries, and invertibility is equivalent to nonzero determinant by A finite square real matrix is invertible if and only if its determinant is nonzero. It therefore has the restricted smooth structure from An open subset of a smooth manifold has a canonical restricted smooth structure. A second basis changes a matrix by A↦P−1AP, a linear diffeomorphism, so this smooth structure is independent of the fixed basis. If n=0, then GL⁡(g) is the singleton containing the unique endomorphism of the zero vector space, with its unique zero-dimensional smooth structure; no determinant criterion is needed.

The next proposition proves that this map is a smooth group representation; after that result it is called the adjoint representation of G.

A Lie group is nonempty and boundaryless. If dim⁡G=0, every Ad⁡g is the unique automorphism of the zero vector space, even when the discrete group itself is nonabelian; dimension one requires no change. No metric, nondegeneracy, interval, endpoint, choice principle, or biconditional is involved. Fixing one finite basis of the supplied finite-dimensional space is a single finite existential instantiation, not a choice from a family.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Adjoint is a smooth Lie-group representation

Statement

Let G be a finite-dimensional real Lie group with Lie algebra g. Its adjoint map is a group homomorphism

Ad⁡:G⟶GL⁡(g),

and it is smooth for the standard smooth structure on GL⁡(g). In particular,

Ad⁡gh=Ad⁡g∘Ad⁡h,Ad⁡e=id⁡g.

Thus Ad⁡ is a smooth finite-dimensional real representation of G on g. No choice principle is required.

Facts & Assumptions

Given: A finite-dimensional real Lie group G with identity e and Lie algebra g=TeG.

[F1]

Conjugation is Cg(h)=ghg−1, and Ad⁡g=d(Cg)e is an invertible linear endomorphism of g; the target GL⁡(g) has its standard basis-independent smooth structure. Conjugation and the adjoint representation of a Lie group.

[F2]

Multiplication and inversion in G are smooth. Lie group.

[F3]

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

[F4]

A finite-dimensional representation is a group homomorphism into the group of invertible linear maps of its representation space. A finite-dimensional representation ρ:G→GL⁡(V) over a field, and its degree.

Proof

technique · direct
1.1F1algebra

For g,h,x∈G, associativity and (gh)−1=h−1g−1 give Cgh(x)=(gh)x(gh)−1=g(hxh−1)g−1=(Cg∘Ch)(x), while Ce=id⁡G.

1.2F1F2

It remains to verify smoothness, not merely pointwise differentiability. Define Φ:G×G→G by Φ(g,x)=gxg−1; [F2] makes Φ smooth. Fix a finite basis of g and a chart at e whose coordinate differential carries it to the standard basis. Around an arbitrary g0, take any chart in the first variable and use the fixed identity chart in the second and target variables. Since Φ(g,e)=e, the matrix entries of Ad⁡g=dxΦ(g,e) in that basis are the first partial derivatives with respect to the second-variable coordinates, evaluated at the identity coordinate. These entries are smooth functions of the first-variable coordinates because the coordinate representative of Φ is smooth. By the standard target structure in [F1], g↦Ad⁡g is smooth near g0, and g0 was arbitrary.

2.1F1F3step 1.1

Differentiate step 1.1 at e. Since Ch(e)=e, the chain rule [F3] gives Ad⁡gh=d(Cg)e∘d(Ch)e=Ad⁡g∘Ad⁡h and Ad⁡e=id⁡g. Hence Ad⁡ is a group homomorphism.

3.1F4step 2.1step 1.2

Step 2.1 supplies the group-homomorphism law and step 1.2 supplies smoothness, so [F4] identifies Ad⁡ as the claimed smooth representation.

4.1F1F2F3F4step 1.1step 2.1step 1.2step 3.1∎

A Lie group is nonempty and boundaryless. If dim⁡G=0, then g=0 and the target is the one-point group, so the map is constant and smooth; dimension one uses the same coordinate argument. No metric, nondegeneracy, interval, or endpoint occurs. The displayed consequences of the homomorphism assertion in the Statement are established in step 2.1. Fixing one finite basis and finitely many charts in a local smoothness test makes no choice from a family, so the proof is choice-free.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Adjoint representation of a Lie algebra

Definition

Let g be a finite-dimensional Lie algebra over F∈{R,C}. For X∈g, its adjoint endomorphism is

ad⁡X∈End⁡F(g),ad⁡X(Y)=[X,Y].

Bilinearity of the bracket makes ad⁡X linear in Y and makes the assignment X↦ad⁡X linear in X. Moreover, the Jacobi identity in Finite-dimensional Lie algebra gives, for every Z∈g,

[ad⁡X,ad⁡Y](Z)=[X,[Y,Z]]−[Y,[X,Z]]=[ [X,Y],Z]=ad⁡[X,Y](Z).

Consequently

ad⁡:g⟶gl(g),X⟼ad⁡X,

is a Lie-algebra homomorphism into the commutator Lie algebra of endomorphisms, where here a Lie-algebra homomorphism means a linear map that preserves the bracket. A linear homomorphism from a Lie algebra into the commutator Lie algebra of endomorphisms is called a representation, and this particular one is the adjoint representation of g. The later general definition of Lie-algebra representations uses exactly this convention but is not a prerequisite for the construction above.

For the zero algebra this is the unique map between zero spaces. Every one-dimensional Lie algebra over the stated fields has zero bracket, so its adjoint representation is zero. Degenerate adjoint maps are allowed; no faithfulness is asserted. The construction is algebraic, boundaryless and endpoint-free, uses no metric or choice principle, and contains no biconditional.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The differential of Ad is ad

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. Under the canonical open-subset identification

TIGL⁡(g)≃End⁡(g),

the differential of the adjoint representation at the identity is

d(Ad⁡)e(X)=ad⁡X(X∈g).

Consequently [ad⁡X,ad⁡Y]=ad⁡[X,Y]G. The countable-choice assumption is used exactly through the supplied smooth invariant-field, tangent-bracket, exponential, and vector-field pushforward interfaces.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with identity e, Lie algebra g=TeG, and X,Y∈g.

[F1]

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

[F2]

The adjoint map is smooth and satisfies Ad⁡g=d(Cg)e. Adjoint is a smooth Lie-group representation, Conjugation and the adjoint representation of a Lie group.

[F3]

Left and right translations are Lg(h)=gh and Rg(h)=hg; the left-invariant extension is YhL=d(Lh)eY. Left and right translations on a Lie group, Left- and right-invariant vector fields, Left-invariant vector fields evaluate isomorphically at the identity.

[F4]

The tangent bracket is characterized by [XL,YL]=[X,Y]GL. Lie bracket on the tangent space of a Lie group.

[F5]

The curve t↦exp⁡(tX) is the one-parameter subgroup and the integral curve of XL through e. One-parameter subgroups are integral curves of left-invariant fields.

[F6]

For the flow Φt of a field Z, LZW=ddt∣0(Φ−t)∗W, and LZW=[Z,W]. The Lie derivative of a vector field, The Lie derivative of a vector field equals the Lie bracket.

[F7]

Diffeomorphism pushforward is defined by its differential on field values. Pushforwards and pullbacks of vector fields by a diffeomorphism.

[F8]

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

[F9]

The adjoint Lie-algebra representation satisfies ad⁡X(Y)=[X,Y] and [ad⁡X,ad⁡Y]=ad⁡[X,Y]. Adjoint representation of a Lie algebra.

Proof

technique · direct
1.1F2F3F7F8algebra

For g,h∈G, the identity Cg∘Lh=LCg(h)∘Cg and the chain rule show that (Cg)∗YL=(Ad⁡gY)L: at the point Cg(h) both sides equal d(LCg(h))e d(Cg)eY.

1.2F3F5F7F8algebra

By [F5] and left invariance, Φt(h)=hexp⁡(tX)=Rexp⁡(tX)(h) is the global flow of XL: differentiating Lh(exp⁡(tX)) gives Xhexp⁡(tX)L. Since left and right translations commute, (Ra)∗YL is left invariant for every a. Therefore left translation fixes that field, and Cexp⁡(tX)=Lexp⁡(tX)∘Rexp⁡(−tX) gives (Cexp⁡(tX))∗YL=(Rexp⁡(−tX))∗YL.

2.1F4F6step 1.1step 1.2

Differentiate the last identity of step 1.2 at t=0. By the inverse-time convention and equality in [F6], its right side has derivative LXLYL=[XL,YL]=[X,Y]GL, where the last equality is [F4]. Step 1.1 identifies the left side with (Ad⁡exp⁡(tX)Y)L. Evaluating the differentiated fields at e thus yields ddt∣0Ad⁡exp⁡(tX)Y=[X,Y]G.

3.1F2F5F8F9step 2.1

The curve t↦exp⁡(tX) has initial velocity X by [F5]. Apply the chain rule [F8] to t↦Ad⁡exp⁡(tX) and then to the linear evaluation map A↦A(Y). Under TIGL⁡(g)=End⁡(g), step 2.1 becomes (d(Ad⁡)eX)(Y)=[X,Y]G=ad⁡X(Y). Since this holds for every Y, d(Ad⁡)eX=ad⁡X.

4.1F9step 3.1

The final commutator identity follows from [F9], now with the map in [F9] identified by step 3.1 with the differential of the group adjoint representation.

5.1F1F2F3F4F5F6F7F8F9step 1.1step 1.2step 2.1step 3.1step 4.1∎

A Lie group is nonempty and boundaryless. If dim⁡G=0, every tangent space in the claim is zero; in dimension one the Lie bracket and both sides are zero, while the same proof applies. Degenerate adjoint maps are allowed. The flows are global, so there is no endpoint issue, and no metric occurs. The only choice use is the stated ACω, inherited through [F2]--[F7]; fixing two tangent vectors and differentiating their specified curves adds no choice. No biconditional is asserted.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Adjoint intertwines the exponential map

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. For every g∈G and X∈g,

gexp⁡G(X)g−1=exp⁡G(Ad⁡gX).

The countable-choice assumption is inherited exactly from exponential naturality.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G, g∈G, and X∈g=TeG.

[F1]

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

[F2]

Conjugation Cg(h)=ghg−1 is a Lie-group automorphism and d(Cg)e=Ad⁡g. Conjugation and the adjoint representation of a Lie group.

[F3]

Every Lie-group homomorphism F satisfies F(exp⁡X)=exp⁡(dFeX), assuming ACω. Exponential map is natural for Lie-group homomorphisms.

Proof

technique · direct
1.1F2F3

Apply exponential naturality [F3] to the conjugation automorphism Cg from [F2]. Since d(Cg)e=Ad⁡g, it gives Cg(exp⁡GX)=exp⁡G(Ad⁡gX). Expanding the definition of Cg is the claimed identity.

2.1F1F2F3step 1.1∎

A Lie group is nonempty and boundaryless. If dim⁡G=0, both sides equal the conjugate of the identity, and dimension one requires no change; X=0 gives e on both sides. No metric, degeneracy, interval, endpoint, or biconditional occurs. The only choice use is the stated ACω inherited through [F3]; fixing one g and one X adds no choice.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Adjoint exponential identity

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. For every X∈g,

Ad⁡exp⁡GX=ead⁡X.

Here, for B∈End⁡(g), the linear-ODE exponential etB denotes the unique solution EB(t) of

EB′(t)=B∘EB(t),EB(0)=I,

and eB=EB(1). The countable-choice assumption is inherited exactly from the supplied exponential and dAd⁡=ad⁡ results.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G with Lie algebra g, and X∈g.

[F1]

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

[F2]

The adjoint map is a smooth representation, so Ad⁡gh=Ad⁡gAd⁡h and Ad⁡e=I. Adjoint is a smooth Lie-group representation.

[F3]

The unique one-parameter subgroup with initial velocity X is the curve t↦exp⁡G(tX). One-parameter subgroups are exactly exponentials. Exponential scales one-parameter subgroups.

[F4]

Under TIGL⁡(g)=End⁡(g), d(Ad⁡)eX=ad⁡X. The differential of Ad is ad.

[F5]

A linear matrix initial-value problem on a compact interval has a unique solution on the whole interval. Linear matrix ODEs have unique global solutions on a fixed interval.

Proof

technique · direct
1.1F2F3F4

Put A(t)=Ad⁡exp⁡G(tX). By [F2]--[F3], A is smooth, A(0)=I, and A(t+s)=A(t)A(s)=A(s)A(t). The chain rule and [F4] give A′(0)=d(Ad⁡)eX=ad⁡X.

2.1step 1.1algebra

Fix t and differentiate A(t+s)=A(s)A(t) with respect to s at zero. Using step 1.1 gives A′(t)=ad⁡X∘A(t) and A(0)=I.

3.1F5step 2.1

In one fixed basis of g, [F5] gives a unique solution of E′(t)=ad⁡XE(t), E(0)=I, on every compact interval containing zero. Solutions on overlapping intervals agree by uniqueness, so they define the global linear-ODE exponential E(t)=etad⁡X without any arbitrary selection. Step 2.1 and uniqueness give A(t)=E(t) on every such interval. Evaluating at t=1 yields Ad⁡exp⁡GX=ead⁡X.

4.1F1F2F3F4F5step 1.1step 2.1step 3.1∎

A Lie group is nonempty and boundaryless. If dim⁡G=0, both sides are the unique endomorphism of the zero space; in dimension one, ad⁡X=0 and the ODE gives both sides equal to I. Degenerate adjoint endomorphisms are allowed. The compact-interval solutions glue globally, so there is no endpoint issue, and no metric occurs. The only choice use is the stated ACω inherited through [F3]--[F4]; one finite basis and uniquely determined ODE solutions add no choice. No biconditional is asserted.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Right-trivialized differential of the Lie-group exponential

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. For Z,V∈g, right translation identifies the differential of the exponential with

d(Rexp⁡G(−Z))exp⁡GZ(d(exp⁡G)ZV)=∑n=0∞ad⁡Zn(V)(n+1)!.

The operator series converges absolutely in any norm and is denoted

ead⁡Z−Iad⁡Z(V),

with the displayed power series—not division by a possibly singular ad⁡Z—as its definition.

More generally, for every finite-dimensional real vector space and every endomorphism B, the linear-ODE exponential used here satisfies

etB=∑n=0∞tnBnn!,

with absolute convergence uniformly on compact t-intervals.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G, and Z,V∈g.

[F1]

Lie-group exponentials are smooth, and t↦exp⁡G(tW) is the integral curve of WL through the identity. The Lie-group exponential map is smooth with identity differential at zero. One-parameter subgroups are integral curves of left-invariant fields.

[F2]

Left and right translations and their differentials give the standard tangent trivializations. Left and right translations on a Lie group.

[F3]

Assuming countable choice, Ad⁡exp⁡G(tZ)=etad⁡Z, where the right side is the linear-ODE exponential. The Axiom of Countable Choice (ACω). Adjoint exponential identity.

[F4]

Linear matrix initial-value problems have unique solutions on compact intervals. Linear matrix ODEs have unique global solutions on a fixed interval.

[F7]

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

Proof

technique · direct
1.1F4F5

Put B=ad⁡Z. In one basis, the operator series S(t)=∑n≥0tnBn/n! converges absolutely and uniformly on compact t-intervals, since its norm is bounded by the scalar exponential majorant ∑n≥0(∣t∣∥B∥)n/n!. Coordinatewise termwise differentiation gives S′(t)=BS(t) and S(0)=I. By [F4]--[F5], uniqueness therefore identifies S(t) with the linear-ODE exponential etB.

1.2F1F2F7algebra

Consider the smooth variation F(s,t)=exp⁡G(t(Z+sV)) and write γ(t)=F(0,t)=exp⁡G(tZ). Right-trivialize its variational field by ξ(t)=d(Rγ(t)−1)γ(t)(∂sF(0,t)). By [F1], ∂tF(s,t)=d(LF(s,t))e(Z+sV). Differentiate this identity in s, commute the two coordinate partial derivatives, and differentiate the right-trivialization using multiplication and inversion. The two terms containing Z cancel, leaving ξ′(t)=Ad⁡γ(t)V and ξ(0)=0.

2.1F3step 1.1

Consequently [F3] gives Ad⁡exp⁡G(tZ)=S(t) for every real t. This is the exact point where ACω is used.

3.1F5F6step 2.1step 1.2

By steps 2.1 and 1.2, ξ′(t)=S(t)V. The uniformly convergent series A(t)=∑n≥0tn+1Bn(V)/(n+1)! has A(0)=0 and, coordinatewise by [F5], A′(t)=S(t)V. Applying [F6] to ξ−A on [0,1] gives ξ(1)=A(1)=∑n≥0Bn(V)/(n+1)!.

4.1F2F7step 3.1

By the definition of F and the chain rule, ∂sF(0,1)=d(exp⁡G)ZV; by the definition of ξ, its value at one is the right translation of that vector by exp⁡G(−Z). Step 3.1 is therefore exactly the asserted formula.

5.1F1F2F3F4F5F6F7step 1.1step 2.1step 1.2step 3.1step 4.1∎

A Lie group is nonempty and boundaryless. In dimension zero both sides are the unique zero vector; in dimension one the bracket vanishes and the formula reduces to dRexp⁡(−Z)dexp⁡Z(V)=V. Singular ad⁡Z is allowed because the quotient notation means its entire power series. The variation uses the compact interval [0,1] including both endpoints. Countable choice is inherited through [F1] and [F3]; one basis and fixed vectors add no choice. No metric dependence or biconditional is asserted.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Baker–Campbell–Hausdorff series

Definition

Let g be a finite-dimensional real Lie algebra and let X,Y∈g. For a nonempty word w=Z1⋯ZN in the two letters X,Y, define its right-nested commutator by

[Z1]R=Z1,[Z1⋯ZN]R=[Z1,[Z2⋯ZN]R](N≥2).

Equivalently, when N≥2, this is ad⁡Z1∘⋯∘ad⁡ZN−1(ZN) in the notation of Adjoint representation of a Lie algebra.

For N≥1, the degree-N Dynkin polynomial is

HN(X,Y)=∑k=1N(−1)k−1kN∑mi,ni≥0, mi+ni>0 (1≤i≤k)∑i=1k(mi+ni)=N[Xm1Yn1⋯XmkYnk]Rm1!n1!⋯mk!nk!.

Here XmYn means a block of m copies of X followed by n copies of Y; it is word notation, not multiplication in g. For fixed N both sums are finite, so HN(X,Y) is well defined using only the vector space operations and Lie bracket supplied by Finite-dimensional Lie algebra.

The formal Baker–Campbell–Hausdorff series is the degree-indexed formal sum

BCH⁡(X,Y):=∑N=1∞HN(X,Y).

It begins

X+Y+12[X,Y]+112[X,[X,Y]]+112[Y,[Y,X]]+⋯ .

Indeed, the N=1 part has the two one-letter blocks and gives X+Y. In degree two, the k=1 block (m1,n1)=(1,1) contributes 12[X,Y]; the two mixed k=2 words contribute −14([X,Y]+[Y,X])=0, and all repeated-letter brackets vanish. Direct collection of the finite degree-three sum gives the two displayed 1/12 terms.

Until convergence is proved, BCH⁡(X,Y) means this formal sequence of homogeneous Lie polynomials, not an element obtained by summing infinitely many vectors. Wherever the series converges, the same notation denotes its sum. The next convergence lemma justifies this analytic meaning on a neighborhood of (0,0).

For the zero Lie algebra every HN is zero. For a one-dimensional real Lie algebra the bracket vanishes, so the formal series is X+Y. No metric, nondegeneracy, interval, endpoint, choice principle, or biconditional is part of this definition.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Local convergence of the Baker–Campbell–Hausdorff series

Statement

Let g be a finite-dimensional real Lie algebra equipped with any norm ∥⋅∥. There is an ε>0 such that Dynkin's series

BCH⁡(X,Y)=∑N≥1HN(X,Y)

converges absolutely whenever ∥X∥+∥Y∥<ε. Moreover, for every 0<r0<ε, its partial sums converge uniformly on

Dr0:={(X,Y):∥X∥+∥Y∥≤r0}.

No assertion here identifies this convergent sum with log⁡(exp⁡Xexp⁡Y); that is the content of the following BCH theorem.

Facts & Assumptions

Given: A finite-dimensional real Lie algebra g with a norm.

[F1]

The degree-N Dynkin polynomial is the stated finite sum of right-nested commutators, and BCH is its formal degree-indexed series. Baker–Campbell–Hausdorff series.

[F2]

The Lie bracket is bilinear. Finite-dimensional Lie algebra.

[F3]

A chosen finite basis gives a bounded coordinate isomorphism for any norm. A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space.

[F4]

Every finite-dimensional normed real vector space is complete. Every finite-dimensional normed space is Banach.

[F5]

The real exponential series converges absolutely everywhere and obeys exp⁡(a+b)=exp⁡(a)exp⁡(b). The exponential series converges absolutely for every real argument. The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y).

[F7]

Proof

technique · direct
1.1F2F3

If g=0, every HN vanishes and the conclusion holds for every positive ε. Otherwise choose one finite basis. By [F2]--[F3], its finitely many structure constants and the bounded coordinate maps give a constant C≥0 such that ∥[U,V]∥≤C∥U∥∥V∥ for all U,V∈g. This chooses one finite witness, not a family.

2.1F1step 1.1induction

Induction on word length now gives ∥[Z1⋯ZN]R∥≤CN−1∏j=1N∥Zj∥ for every right-nested commutator in [F1].

2.2F1step 1.1cases

If C=0, all brackets vanish, so [F1] gives H1(X,Y)=X+Y and HN(X,Y)=0 for N≥2; take ε=1. Hence suppose C>0 and put ε=1/(4C).

3.1F5F6F7step 2.2

Fix 0<r0<ε and put R=Cr0<1/4. For a=C∥X∥, b=C∥Y∥ and (X,Y)∈Dr0, [F6] shows that the sum of the scalar weights ambn/(m!n!) over a block of positive total degree is q(a,b)=exp⁡(a+b)−1, and its degree-d part is (a+b)d/d!≤Rd/d!. Thus these coefficients are bounded degree by degree by those of q0:=∑d≥1Rd/d!. Since R<1/4 and d!≥1, [F5]--[F7] give 0≤q0≤∑d≥1(1/4)d=1/3<1.

4.1F1F7step 2.1step 3.1algebra

Apply step 2.1 to the formula in [F1]. For a k-block summand of total degree N, absorb CN into its scalar letter weights and retain the factor 1/C. Since 1/N≤1, the sum of the norms of all homogeneous terms, uniformly for (X,Y)∈Dr0, is bounded by the nonnegative degree expansion of 1C∑k≥1q0k/k≤1C∑k≥1q0k, which converges by [F7]. In particular, the resulting degree majorants MN satisfy ∥HN(X,Y)∥≤MN on Dr0 and ∑NMN<∞.

5.1F4step 4.1

For each (X,Y)∈Dr0, step 4.1 makes the partial sums Cauchy by the triangle inequality, and [F4] supplies their limit. Moreover, the norm of every tail is bounded by the corresponding scalar tail ∑N>mMN, independently of (X,Y); that tail tends to zero. Hence the convergence is absolute and uniform on Dr0.

6.1F1F2step 1.1step 2.2step 5.1∎

Any pair with ∥X∥+∥Y∥<ε lies in some Dr0 with ∥X∥+∥Y∥<r0<ε, so step 5.1 proves both claims. The zero and one-dimensional cases are included; in dimension one the bracket is zero. Degenerate brackets are allowed. There is no interval or endpoint, no metric beyond the arbitrary norm in the statement, no choice principle beyond choosing one finite basis, and no biconditional.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Baker–Campbell–Hausdorff theorem

Statement

Assume ACω. Let G be a finite-dimensional real Lie group with Lie algebra g. For every chosen local logarithm there is an open neighborhood W of (0,0) in g×g such that Dynkin's series converges for (X,Y)∈W and

log⁡G(exp⁡G(X)exp⁡G(Y))=BCH⁡(X,Y).

Consequently, for every (X,Y)∈W,

exp⁡G(X)exp⁡G(Y)=exp⁡G(BCH⁡(X,Y)).

The neighborhood can be chosen inside any convergence ball supplied by the preceding convergence lemma and so that the product remains in the fixed domain of log⁡G.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group G, a fixed norm on g, and one local logarithm log⁡G:U→V associated with exp⁡G∣V.

[F1]

The local logarithm is the inverse of the exponential on the specified open neighborhoods, and Dynkin's BCH series converges absolutely on a sum-norm ball and uniformly on smaller closed balls. Local logarithm on a Lie group. Local convergence of the Baker–Campbell–Hausdorff series.

[F2]

Right-trivialization of dexp⁡Z is the entire operator series D(ad⁡Z)=∑n≥0ad⁡Zn/(n+1)!, and the linear-ODE exponential is its operator power series, uniformly on compact parameter intervals. Right-trivialized differential of the Lie-group exponential.

[F3]

The adjoint map is a smooth representation and, assuming countable choice, Ad⁡exp⁡Z=ead⁡Z. The Axiom of Countable Choice (ACω). Adjoint is a smooth Lie-group representation. Adjoint exponential identity.

[F4]

The curve t↦exp⁡G(tZ) is the integral curve of ZL through e; translations give the tangent trivializations; and differentials obey the chain rule. One-parameter subgroups are integral curves of left-invariant fields. Left and right translations on a Lie group. The chain rule for differentials of smooth maps.

[F5]

Formal exponential and logarithm over a commutative rational algebra are inverse, where log⁡(1+w)=∑j≥1(−1)j−1wj/j. Formal exponential, logarithm, and binomial powers over a commutative Q-algebra. Formal exp⁡ and log⁡ are inverse homomorphisms and formal binomial powers obey the expected addition laws.

[F6]

The scalar exponential series converges everywhere, and a geometric series converges when its ratio has absolute value less than one. The exponential series converges absolutely for every real argument. For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges.

Proof

technique · direct analytic identification with Dynkin's series
1.1F1F4F7

By [F1], choose a BCH convergence ball. The smooth map Φ(t,X,Y)=exp⁡G(tX)exp⁡G(tY) sends [0,1]×{(0,0)} to e∈U. Apply the tube lemma to Φ−1(U) and intersect the resulting neighborhood of (0,0) with a sufficiently small sum-norm ball. For (X,Y) in this neighborhood, put g(t)=Φ(t,X,Y) and H(t)=log⁡G(g(t)); then H is smooth, H(0)=0, and exp⁡G(H(t))=g(t) for all 0≤t≤1.

2.1F2F3F4step 1.1

Right-trivializing the derivative of the product and using the two one-parameter-subgroup equations gives d(Rg(t)−1)g(t)g′(t)=X+Ad⁡exp⁡G(tX)Y=X+etad⁡XY. Applying [F2] to g(t)=exp⁡G(H(t)) therefore gives D(A(t))H′(t)=X+etad⁡XY, where A(t)=ad⁡H(t) and D(A)=∑n≥0An/(n+1)!.

2.2F2F3F7step 1.1

Since Ad⁡ is a representation, [F3] and step 1.1 give eA(t)=Ad⁡exp⁡H(t)=etad⁡Xetad⁡Y. Put P(t)=etad⁡Xetad⁡Y−I. Continuity and the tube lemma allow a further shrinking, uniform in t∈[0,1], so that ∥P(t)∥<q<1 and H(t) remains in a fixed small coordinate ball.

3.1F5F6step 2.1step 2.2

Define Q(P)=∑j≥0(−1)jPj/(j+1). It converges absolutely for ∥P∥<1 by [F6]. In the commutative formal subalgebra generated by one indeterminate z, [F5] gives log⁡(ez)=z, hence D(z)Q(ez−1)=1. Absolute operator convergence permits substitution z=A(t) and coefficientwise multiplication, so Q(P(t)) is the two-sided inverse of D(A(t)). Thus step 2.1 becomes H′(t)=∑j≥0(−1)jP(t)j(X+etad⁡XY)/(j+1).

4.1F2F6F7step 2.2step 3.1

Expand P(t) by [F2]: P(t)=∑m,n≥0, m+n>0tm+nad⁡Xmad⁡Yn/(m!n!). The bound ∥P(t)∥≤q<1, together with exponential scalar majorants after one further shrinking, makes the expansions in step 3.1 jointly absolutely and uniformly convergent on [0,1]. In finite coordinates [F7] therefore permits termwise multiplication, regrouping, and integration.

5.1F1step 4.1algebra

A term with k−1 positive blocks from P(t)k−1 followed by the terminal X has word degree N, coefficient (−1)k−1/k, and power tN−1; a term followed by etad⁡XY has the same description, with final block XmY and again power tN−1. Every other possible final block in Dynkin's formula has at least two terminal equal letters and its right-nested commutator is zero. Hence integration from zero to one contributes the factor 1/N and gives exactly the full degree-N Dynkin polynomial HN(X,Y).

6.1F1F7step 1.1step 4.1step 5.1

By vector-valued FTC and step 1.1, H(1)=∫01H′(t) dt. Steps 4.1–5.1 and the uniform convergence in [F1] identify this integral with ∑N≥1HN(X,Y)=BCH⁡(X,Y). Since H(1)=log⁡G(exp⁡GXexp⁡GY), the logarithmic identity follows; applying exp⁡G and using [F1] gives the asserted product identity.

7.1F1F2F3F4F5F6F7step 1.1step 2.1step 2.2step 3.1step 4.1step 5.1step 6.1∎

A Lie group contains its identity. In dimension zero the identities are the unique identities, and in dimension one the bracket vanishes so BCH is X+Y and the local product is additive in exponential coordinates. No adjoint endomorphism is assumed invertible: step 3.1 inverts D(A) by a convergent series and never divides by A. Both endpoints of [0,1] occur in steps 1.1 and 6.1. The only choice principle is ACω, inherited exactly through the local logarithm, exponential, and adjoint-exponential suppliers in [F1]–[F4]; all shrinkings select finitely many single witnesses. No metric independence beyond the arbitrary auxiliary norm and no biconditional is asserted.

CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The local Lie-group law is determined by the Lie bracket

Statement

Assume ACω. In exponential coordinates near the identity of a finite-dimensional real Lie group, multiplication is

(X,Y)⟼BCH⁡(X,Y).

Thus the germ of multiplication at the identity is determined by the Lie-algebra bracket.

Facts & Assumptions

Given: ACω, a finite-dimensional real Lie group, and the local logarithm and BCH neighborhood below.

[F1]

On a sufficiently small neighborhood, log⁡G(exp⁡GXexp⁡GY)=BCH⁡(X,Y). Baker–Campbell–Hausdorff theorem.

[F2]

The local logarithm is inverse to the exponential on its stated domain. Local logarithm on a Lie group.

[F3]

Countable choice is the assumption inherited by both suppliers. The Axiom of Countable Choice (ACω).

Proof

technique · direct
1.1F1F2

Choose the neighborhood supplied by [F1], already shrunk inside the domain in [F2]. In the chart log⁡G, the coordinate of the product of the points with coordinates X and Y is log⁡G(exp⁡GXexp⁡GY)=BCH⁡(X,Y).

2.1F1step 1.1

Dynkin's series is built solely from addition, scalar multiplication, and the Lie bracket, so step 1.1 shows that the multiplication germ is determined by that bracket.

3.1F1F2F3step 1.1step 2.1∎

The identity makes the group nonempty. In dimensions zero and one the formula respectively reduces to the unique product and to X+Y. Degenerate adjoint maps are allowed; no division by them occurs. There is no interval, endpoint, metric, or biconditional. ACω is used exactly through [F1]–[F2], and the one neighborhood choice adds no family choice.

CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Commuting nearby group elements have commuting logarithms under the stated domain hypotheses

Statement

Assume ACω. There is an exponential neighborhood U of the identity such that, whenever g,h∈U commute and X=log⁡Gg, Y=log⁡Gh, one has [X,Y]=0.

Facts & Assumptions

Given: The stated group and local logarithm.

[F1]

The local logarithm is inverse to the exponential on its fixed domain. Local logarithm on a Lie group.

[F2]

Conjugation intertwines exponential, and Ad⁡exp⁡X=ead⁡X under countable choice. Adjoint intertwines the exponential map. Adjoint exponential identity. The Axiom of Countable Choice (ACω).

[F3]

The entire operator series D(A)=∑n≥0An/(n+1)! has constant term I. Right-trivialized differential of the Lie-group exponential.

Proof

technique · direct
1.1F1F2F3

The map (g,Y)↦Ad⁡gY is continuous and equals Y at g=e. Shrink the logarithm neighborhood so that Y and Ad⁡gY both lie in its exponential chart whenever g,h∈U and Y=log⁡Gh. Since the power series D(ad⁡X) depends continuously on X and equals I at X=0, shrink once more so it is invertible for every X=log⁡Gg.

2.1F1F2step 1.1

If gh=hg, then ghg−1=h. With h=exp⁡GY, [F2] gives exp⁡G(Ad⁡gY)=exp⁡GY. Both exponents lie in the injectivity domain fixed in step 1.1, so Ad⁡gY=Y.

3.1F2F3step 1.1step 2.1algebra

Write g=exp⁡GX. By [F2], (ead⁡X−I)Y=0. The power-series identity eA−I=D(A)A gives D(ad⁡X)[X,Y]=0; invertibility from step 1.1 yields [X,Y]=0.

4.1F1F2F3step 1.1step 2.1step 3.1∎

The group is nonempty. In dimensions zero and one the conclusion is automatic. Singular ad⁡X is allowed because only D(ad⁡X), close to I, is inverted. There is no interval, endpoint, metric, or biconditional. ACω is inherited exactly through [F1]–[F3]; finitely many neighborhood shrinkings add no choice.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-09-14Open item page →

Real and complex Lie groups

Definition

A real Lie group is a Lie group in the sense of Lie group: its manifold and its multiplication and inversion are real smooth.

A complex Lie group is a group equipped with a finite-dimensional complex manifold structure such that multiplication and inversion are holomorphic in complex charts in the sense of Holomorphic maps Cm→Cn and the complex Jacobian matrix when the chart dimension is positive. In complex dimension zero, charts take values in the singleton C0={0}; every map between such chart domains is holomorphic by the zero-dimensional convention, with the unique zero differential and empty Jacobian. This supplies the case excluded by the cited positive-dimensional holomorphy definition. In positive complex dimension, the holomorphic chain rule (The composite of holomorphic maps is holomorphic and its complex Jacobian is the product) makes left translations biholomorphic with complex-linear differentials. Consequently the invariant-field construction gives a complex-bilinear tangent Lie bracket. In complex dimension zero the tangent space is zero, so the same conclusion holds directly without invoking that positive-dimensional chart interface.

The underlying real manifold of a complex Lie group is a real Lie group. This item fixes terminology only; it does not rebuild complex analytic Lie theory. The zero-dimensional group is included. A Lie group contains its identity, so there is no empty case. No metric, nondegeneracy, interval, endpoint, choice principle, or biconditional occurs.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The exponential map of a Lie group is a group homomorphism

Statement refuted

The exponential map of a Lie group is a group homomorphism from its additive Lie algebra.

Facts & Assumptions

Given: The upper-unitriangular real 3-by-3 matrix group and X=E01, Y=E12.

[F1]

Matrix units have their standard entries, and the row-by-column product therefore gives EijEkl=δjkEil. Matrix units Eij and the Kronecker delta. Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes.

[F2]

Matrix multiplication and the identity matrix have their usual entrywise meaning. Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes.

[F3]

The scalar exponential series converges absolutely. The exponential series converges absolutely for every real argument.

Refutation

technique · counterexample
1.1F1F2F3algebra

By [F1], X2=Y2=0, XY=E02, YX=0, and (X+Y)2=E02 while (X+Y)3=0. The finite matrix exponential series therefore gives eX=I+X, eY=I+Y, and eX+Y=I+X+Y+12E02.

2.1F1F2step 1.1algebra

Direct multiplication gives eXeY=(I+X)(I+Y)=I+X+Y+E02, which differs from eX+Y in its (0,2) entry. Thus exponential does not preserve addition.

3.1F1F2F3step 1.1step 2.1∎

The witness is a nonempty connected three-dimensional matrix Lie group. No zero- or one-dimensional group can exhibit this particular noncommutative failure. No metric, nondegeneracy, interval, endpoint, choice principle, or biconditional occurs.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The exponential map is globally injective on every connected Lie group

Statement refuted

The exponential map is globally injective on every connected Lie group.

Facts & Assumptions

Given: The additive quotient G=R/Z with its standard one-dimensional quotient charts.

[F1]

A Lie-group exponential evaluates the one-parameter subgroup with the specified initial velocity at time one. Exponential map of a Lie group.

[F2]

A Lie group has smooth multiplication and inversion. Lie group.

Refutation

technique · counterexample
1.1F2F3

Addition and negation descend to smooth operations in the quotient charts, so G is a one-dimensional Lie group. The quotient map π:R→G is continuous and surjective; since R is connected, [F3] makes G connected.

2.1F1step 1.1

For X∈T0G≃R, the curve γX(t)=[tX] is a one-parameter subgroup with initial velocity X. Hence [F1] gives exp⁡G(X)=[X].

3.1step 2.1algebra

In particular, exp⁡G(0)=[0]=[1]=exp⁡G(1) although 0≠1. Thus the exponential is not globally injective.

4.1F1F2F3step 1.1step 2.1step 3.1∎

The witness is nonempty, connected, and one-dimensional, so it also covers the lowest positive dimension. No metric, degeneracy, endpoint, choice, or biconditional occurs. The zero-dimensional connected case is harmless but cannot rescue the universal claim.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The exponential map is surjective on every connected Lie group

Statement refuted

Assume ACω. The exponential map is surjective on every connected Lie group.

Facts & Assumptions

Given: ACω, G=GL⁡2+(R) and A=diag⁡(−2,−1/2).

[F1]

The Lie-group exponential is defined from its invariant integral curve. Exponential map of a Lie group.

[F3]

Linear matrix ODEs have unique compact-interval solutions, and the scalar exponential series converges absolutely. Linear matrix ODEs have unique global solutions on a fixed interval. The exponential series converges absolutely for every real argument.

[F4]
[F5]

ACω is countable choice; it is required by the exponential-map interface [F1]. The Axiom of Countable Choice (ACω).

Refutation

technique · counterexample
1.1F2F4algebra

The open matrix group G is connected. Indeed, [F4] writes every B∈G as B=SU with U positive definite and S∈SO⁡(2). The path (1−t)U+tI stays positive definite, and every S∈SO⁡(2) is a rotation joined to I by varying its angle. Thus B is path connected to I. Also det⁡A=1, so A∈G; explicitly t↦R(πt)diag⁡(2t,2−t) joins I to A.

1.2F1F3algebra

For a real matrix X, the absolutely convergent series E(t)=∑n≥0tnXn/n! solves E′=XE and E(0)=I. By [F1] and [F3], uniqueness identifies E(1) with exp⁡GX. In particular, X commutes with exp⁡GX.

2.1F2F3step 1.2algebra

If exp⁡GX=A, step 1.2 says XA=AX. Because A has two distinct real eigenvalues, this equation forces X to preserve each coordinate line and hence to be diagonal, say X=diag⁡(u,v). Then exp⁡GX=diag⁡(eu,ev) has positive diagonal entries, contradicting the two negative entries of A.

3.1F1F2F3F4F5step 1.1step 1.2step 2.1∎

Thus A is not exponential although G is nonempty, connected, and four-dimensional. The determinant is nonzero and no degeneracy is hidden. The paths include both endpoints. The Euclidean inner product in [F4] is an explicit finite-dimensional witness and invokes no metric-existence theorem. Countable choice is assumed exactly to use [F1]; no additional choice or biconditional occurs, and zero and one dimensions cannot invalidate this explicit counterexample.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Right-invariant fields identify T_eG with the same bracket as left-invariant fields

Statement refuted

Ordinary right-invariant fields identify TeG with the same Lie bracket as ordinary left-invariant fields.

Facts & Assumptions

Given: ACω and the upper-unitriangular 3-by-3 group.

[F1]

Right-invariant extensions carry the negative of the tangent bracket. Right-invariant fields carry the opposite Lie bracket.

[F2]

Matrix units obey EijEkl=δjkEil. Matrix units Eij and the Kronecker delta.

[F3]

Countable choice is the exact assumption inherited from [F1]. The Axiom of Countable Choice (ACω).

Refutation

technique · counterexample
1.1F2algebra

Put X=E12 and Y=E23. By [F2], their left-invariant tangent bracket is [X,Y]=XY−YX=E13≠0.

2.1F1step 1.1

By [F1], the corresponding right-invariant fields satisfy [XR,YR]=−[X,Y]R=−E13R, not E13R. This disproves the same-bracket assertion.

3.1F1F2F3step 1.1step 2.1∎

The witness is nonempty and three-dimensional; dimensions zero and one have zero bracket and cannot witness the sign error. There is no metric, degeneracy, interval, endpoint, or biconditional. ACω is propagated exactly through [F1], with no additional choice.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Every continuous group homomorphism is smooth by definition

Statement refuted

Every continuous group homomorphism between Lie groups is smooth by definition.

Facts & Assumptions

Given: The library definition of a Lie-group homomorphism.

[F1]

A Lie-group homomorphism is required to be both a group homomorphism and a smooth map. Lie-group homomorphism, isomorphism, and automorphism.

Refutation

technique · direct comparison of hypotheses
1.1F1

By [F1], smoothness is an explicit defining hypothesis. Continuity alone is not the same syntactic condition and the definition contains no implication from continuity to smoothness.

2.1F1step 1.1

The automatic-smoothness assertion for continuous homomorphisms is a substantive theorem requiring proof; it cannot be obtained merely by unpacking [F1]. Therefore the qualification “by definition” is false even though the separate theorem is true.

3.1F1step 1.1step 2.1∎

This is a claim about logical provenance, so dimensions zero and one do not alter it. Lie groups are nonempty; no metric, degeneracy, interval, endpoint, choice, example witness, or biconditional occurs.

False statementConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Differential at the identity determines a homomorphism from a disconnected Lie group

Statement refuted

A homomorphism from a disconnected Lie group is determined by its differential at the identity.

Facts & Assumptions

Given: The finite discrete Lie group G=Z/2Z.

[F1]

A smooth group homomorphism is a Lie-group homomorphism. Lie-group homomorphism, isomorphism, and automorphism.

[F2]

A discrete finite group is a zero-dimensional Lie group: every map between discrete charts is smooth. Lie group.

Refutation

technique · counterexample
1.1F1F2

Let F:G→G be the identity and let H:G→G be the trivial homomorphism. Both are smooth by discreteness and hence are Lie-group homomorphisms by [F1]–[F2], but F(1)=1≠0=H(1).

2.1F2step 1.1

The tangent space of a zero-dimensional manifold at every point is the zero vector space. Thus dF0 and dH0 are both the unique map 0→0, despite F≠H.

3.1F1F2step 1.1step 2.1∎

The witness is nonempty, zero-dimensional, and disconnected; it shows exactly why connectedness cannot be dropped. No metric, degeneracy beyond the deliberately zero tangent space, interval, endpoint, choice, or biconditional occurs.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedaudited 2026-09-14Open item page →

General and special linear Lie groups

Example

Assume ACω and let n≥1. The open matrix group GL⁡n(R) has Lie algebra Mn(R) with bracket [X,Y]=XY−YX. Its subgroup

SL⁡n(R)={A:det⁡A=1}

is an embedded Lie group with Lie algebra sln(R)={X:tr⁡X=0}.

Facts & Assumptions

Given: An integer n≥1 and the standard Euclidean structure on Mn(R).

[F1]

Lie groups have smooth multiplication and inversion, and the tangent bracket is defined through left-invariant fields. Lie group. Lie bracket on the tangent space of a Lie group.

[F3]

A regular level is embedded and its tangent space is the kernel of the differential. A regular level set is an embedded submanifold. The tangent space of a regular level set is the kernel.

[F4]

Countable choice is inherited by the tangent-bracket supplier. The Axiom of Countable Choice (ACω).

Verification

technique · direct
1.1F1F2algebra

The set det⁡≠0 is open in Mn(R), and matrix multiplication and inversion are smooth there, so it is a Lie group with tangent space Mn(R) at I. Its left-invariant field generated by X is A↦AX; differentiating two such fields gives bracket XY−YX.

1.2F2F3algebra

Expanding the determinant by permutations shows det⁡(I+tX)=1+ttr⁡X+O(t2), hence d(det⁡)I(X)=tr⁡X. At every A∈det⁡−1(1), multiplication by A transports this differential to a nonzero functional, so 1 is a regular value. By [F3], SL⁡n is embedded and its tangent space at I is the trace-zero kernel.

2.1F1F2step 1.1step 1.2algebra

Determinant multiplicativity and det⁡(A−1)=(det⁡A)−1 make the level set a subgroup, so its induced operations are smooth and it is a Lie group. The commutator bracket preserves trace zero because tr⁡(XY)=tr⁡(YX).

3.1F1F2F3F4step 1.1step 1.2step 2.1∎

For n=1, sl1=0. Singular tangent matrices are allowed. No interval, endpoint, metric choice, or biconditional occurs. ACω is used only through the current tangent-bracket interface [F1]; the displayed Euclidean coordinates are finite and add no choice.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Orthogonal and special orthogonal Lie groups

Example

Assume ACω. The groups

O(n)={A:ATA=I},SO(n)={A∈O(n):det⁡A=1}

are embedded Lie groups, and both have tangent Lie algebra

so(n)={X:XT+X=0}

at the identity.

Facts & Assumptions

Given: Real n-by-n matrices.

[F1]

GL⁡n is a matrix Lie group with commutator tangent bracket. General and special linear Lie groups.

[F2]

Transpose reverses matrix products. The transpose AT of a matrix.

[F3]

A constant-rank level set has the induced embedded manifold structure and tangent kernel. The constant-rank theorem for manifolds.

[F4]

Countable choice is inherited through [F1]. The Axiom of Countable Choice (ACω).

Verification

technique · direct
1.1F1F2F3algebra

Let F:GL⁡n(R)→Sym⁡n(R) be F(A)=ATA. Its differential is dFA(X)=XTA+ATX. This is surjective: for symmetric S, take X=12A−TS. Hence [F3] makes F−1(I)=O(n) an embedded submanifold, and it is a subgroup by [F2].

2.1F1F2step 1.1algebra

At A=I, the tangent kernel is XT+X=0. It is closed under commutators because (XY−YX)T=YTXT−XTYT=−(XY−YX) for skew-symmetric X,Y.

3.1F1F2step 1.1step 2.1algebra

On O(n), det⁡(A)2=det⁡(ATA)=1, so determinant takes only the values 1 and −1. Its 1-fibre is therefore open and closed in O(n) and is an embedded Lie subgroup with the same identity tangent space.

4.1F1F2F3F4step 1.1step 2.1step 3.1∎

For n=0 both groups are the one-point group; for n=1, so(1)=0, O(1) is discrete, and SO(1) is trivial. No interval, endpoint, nondegeneracy beyond invertibility in GL⁡n, metric choice, or biconditional occurs. ACω is propagated only through [F1].

ExampleConstruction: AI-adaptedVerification: AI-adaptedaudited 2026-09-14Open item page →

Unitary and special unitary Lie groups

Example

Assume ACω and let n≥1. Regarded as real Lie groups,

U(n)={A∈GL⁡n(C):A∗A=I},SU(n)={A∈U(n):det⁡A=1}

have Lie algebras

u(n)={X:X∗+X=0},su(n)={X∈u(n):tr⁡X=0}.

Facts & Assumptions

Given: An integer n≥1 and complex matrices viewed as a finite-dimensional real vector space.

[F1]

A Lie group has smooth multiplication and inversion, and its tangent bracket is the bracket of left-invariant fields. Lie group. Lie bracket on the tangent space of a Lie group.

[F2]

Over the field C, a positive-sized matrix is invertible exactly when its determinant is nonzero, and its inverse is its adjugate divided by that determinant. A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit. If det⁡(A) is a unit, then A−1=det⁡(A)−1adj⁡(A).

[F3]

Complex conjugation supplies the conjugate transpose A∗. Real and imaginary parts, complex conjugation, and modulus.

[F4]

Constant-rank level sets are embedded with tangent kernel. The constant-rank theorem for manifolds.

[F6]

Countable choice is inherited through the tangent-bracket supplier in [F1]; the finite matrix and level-set calculations need no further choice. The Axiom of Countable Choice (ACω).

Verification

technique · direct
1.1F1F2F3F4F5algebra

Regard Mn(C) as R2n2. The complex determinant is a finite polynomial in matrix entries by [F5], hence its real and imaginary parts are real polynomials. By [F2], GL⁡n(C)={A:det⁡A≠0} is open in this real vector space; multiplication is polynomial and inversion is real smooth there by the adjugate formula. Thus it is a real Lie group by [F1]. Its left-invariant field with identity value X is A↦AX; differentiating these linear fields gives the tangent bracket [X,Y]=XY−YX in the convention of [F1]. Now F(A)=A∗A maps this open group smoothly into the real vector space of Hermitian matrices and has dFA(X)=X∗A+A∗X. For Hermitian S, X=12A−∗S maps to S, so [F4] makes U(n)=F−1(I) embedded; the adjoint-product identities make it a subgroup. At I its tangent kernel is X∗+X=0.

2.1F4F5step 1.1algebra

For A∈U(n), ∣det⁡A∣2=det⁡(A∗A)=1, so determinant maps U(n) into the unit circle. Near 1 that circle has the real coordinate z↦Im⁡z on the arc Re⁡z>0. Differentiating the finite determinant formula at I gives d(det⁡)I(X)=tr⁡X; on skew-Hermitian X this is imaginary and every imaginary scalar occurs from a diagonal X. Left multiplication by any A∈SU(n) transports this surjectivity to A. Hence 1 is a regular value of the circle-valued determinant map and [F4] makes SU(n) embedded in U(n), with tangent kernel tr⁡X=0 at I. Its subgroup operations are smooth by restriction.

3.1F1F3step 1.1step 2.1algebra

Both tangent spaces are closed under commutator: adjoint reverses products, and trace of a commutator vanishes by finite reindexing. Hence they are the asserted Lie algebras.

4.1F1F2F3F4F5F6step 1.1step 2.1step 3.1∎

At n=1, u(1)=iR and su(1)=0; n=0 is excluded by the Statement. No interval, endpoint, arbitrary metric choice, or biconditional occurs. The ambient determinant is nonzero exactly on GL⁡n(C) by [F2]. ACω is inherited through [F1]; finite coordinates add no choice.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Matrix exponential as the Lie-group exponential

Example

Assume ACω. Let G be a matrix Lie group, meaning an embedded Lie subgroup of GL⁡n(R), and identify g=TIG with its image in Mn(R). Then

exp⁡G(X)=eX:=∑k=0∞Xkk!(X∈g).

In particular, the ordinary matrix exponential of every X∈g belongs to G.

Facts & Assumptions

Given: The embedded Lie subgroup G⊆GL⁡n(R) and X∈TIG.

[F1]

The Lie exponential is the time-one value of the one-parameter subgroup with initial velocity X. Exponential map of a Lie group.

[F2]

The scalar exponential series has infinite radius of convergence. The exponential series converges absolutely for every real argument.

[F3]

Linear matrix initial-value problems have unique solutions on each compact interval. Linear matrix ODEs have unique global solutions on a fixed interval.

[F4]

Matrix multiplication and the identity matrix have their usual coordinate definitions. Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes.

[F5]

The construction of [F1] carries the stated countable-choice assumption. The Axiom of Countable Choice (ACω).

Verification

technique · direct comparison of two matrix ODEs
1.1F2F4algebra

Suppose first that n≥1 and put ∥A∥∞=max⁡i,j∣aij∣. The row-by-column formula [F4] gives ∥AB∥∞≤n∥A∥∞∥B∥∞, and hence ∥Xk∥∞≤nk−1∥X∥∞k for k≥1. Thus [F2] dominates the matrix series and its termwise derivative uniformly on every compact t-interval by scalar exponential series. Consequently, for E(t)=∑k≥0tkXk/k!, termwise differentiation is valid for every real t, and [F4] gives E′(t)=XE(t)=E(t)X and E(0)=I. When n=0 this is the constant identity curve directly.

2.1F1F3step 1.1

Let γX:R→G be the subgroup from [F1], viewed as a matrix curve. Its velocity at t is the left translate of X, so γX′(t)=γX(t)X and γX(0)=I. Transposing gives (γXT)′=XTγXT. Step 1.1 likewise gives (ET)′=XTET with E(0)T=I. On every compact interval containing zero, [F3] makes these transposed solutions equal. Thus γX(t)=E(t) for all t∈R.

3.1F1F2F3F5step 2.1∎

Evaluating step 2.1 at t=1 proves the displayed formula and, because γX(1)∈G, also proves eX∈G. For n=0 both sides are the identity of the one-point group, and for X=0 both equal I; no invertibility or spectral hypothesis on X is used. The parameter is global, so t=1 is not an endpoint issue. This is an equality, not an iff claim. ACω is used exactly through [F1]; the series and ODE comparison add no choice.

Sources