Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Continuous homomorphisms between Lie groups are smooth

Statement

Assume ACω. Every continuous group homomorphism F:G→H between finite-dimensional real Lie groups is smooth.

Facts & Assumptions

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

[A1]

Closed subgroups have embedded Lie-group structures under countable choice. The Axiom of Countable Choice (ACω), Cartan closed subgroup theorem.

[F1]

Homeomorphic nonempty manifolds have equal intrinsic dimension. Local homology detects manifold dimension, interior, and boundary.

[F2]

A smooth map with invertible differential is locally a diffeomorphism. The smooth inverse function theorem on manifolds.

[F3]

For a smooth Lie-group homomorphism P, P(exp⁡X)=exp⁡(dPeX). Exponential map is natural for Lie-group homomorphisms.

Proof

technique · the closed graph subgroup
1.1A1givenalgebra

The graph ΓF={(g,F(g)):g∈G} is a subgroup of G×H. It is closed: if (g,h) is not on the graph, then h≠F(g), and continuity of F together with Hausdorffness of H gives product neighborhoods of (g,h) disjoint from the graph. By [A1], ΓF is an embedded Lie subgroup.

2.1F1step 1.1

The first projection P:ΓF→G is a smooth Lie-group homomorphism and a homeomorphism, with continuous inverse g↦(g,F(g)). Manifold charts and [F1] therefore give dim⁡ΓF=dim⁡G.

3.1F3step 2.1algebra

We show that dP(e,e) is injective. If X is in its kernel, [F3] gives P(exp⁡ΓF(tX))=exp⁡G(t,dP(e,e)X)=e for every t. The algebraic kernel of P is the singleton (e,e), so this one-parameter subgroup is constant; differentiating it at zero gives X=0. Equal dimensions from step 2.1 now make dP(e,e) an isomorphism.

4.1F2step 3.1

Translation of the homomorphism identity makes dP invertible everywhere. By [F2], P has smooth local inverses around every point. Since the set-theoretic inverse is unique, these local inverses agree with the global continuous inverse P−1, so P−1 is smooth.

5.1A1F3step 3.1step 4.1∎

Let Q:ΓF→H be the second projection. Then F=Q∘P−1 is smooth. Zero-dimensional and disconnected groups are included; no injectivity or surjectivity of F is assumed. The exponential argument in step 3.1 is the needed correction to the scaffold: a smooth homeomorphism between equal-dimensional manifolds need not have invertible differential. Countable choice is used through [A1] and [F3].

Depends on

Used by

Dependency tree · two levels

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

Sources