Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Kernel of the infinitesimal orbit map

Statement

Assume ACω. For a smooth left action of G on M and x∈M, the linear infinitesimal orbit map

g⟶TxM,X⟼XM(x)

has kernel gx=TeGx. Its image is the tangent space at x of the orbit with its canonical injectively immersed structure.

Facts & Assumptions

Given: A smooth left action, a point x∈M, its orbit map Φx(g)=g⋅x, and quotient map q:G→G/Gx.

[F1]

With the standing minus convention, XM(x)=d(Φx)e(−X). Fundamental vector fields for a left action. Orbits, stabilizers, and orbit maps of smooth actions.

[F2]

The stabilizer is a closed embedded Lie subgroup. Stabilizers are closed embedded Lie subgroups.

[F3]

A constant-rank map has local normal form (u,v)↦(u,0). The constant-rank theorem for manifolds.

[F4]

The quotient G/Gx is smooth, q is a submersion, and TeGx(G/Gx)≃g/gx. Quotient manifold by a closed Lie subgroup. Tangent space of a homogeneous quotient.

[F6]

The preceding suppliers carry countable choice. The Axiom of Countable Choice (ACω).

Proof

technique · constant rank followed by quotienting the kernel
1.1givenalgebra

For every g,h∈G, Φx(gh)=g⋅Φx(h). Left translation by g on G and action by g on M are diffeomorphisms, so differentiating shows that d(Φx)g has the same rank as d(Φx)e. Thus Φx has constant rank.

2.1F2F3step 1.1

The fibre Φx−1(x) is Gx by definition. Apply the local normal form [F3] at e: the tangent space of this fibre is the kernel of d(Φx)e. Because [F2] gives the fibre its embedded structure, ker⁡d(Φx)e=TeGx=gx.

3.1F1step 2.1algebra

By [F1], the infinitesimal map is −d(Φx)e. Multiplication by −1 does not change kernel or image, so step 2.1 proves ker⁡(X↦XM(x))=gx and identifies its image with im⁡d(Φx)e.

4.1F4F5step 2.1step 3.1

The orbit map is constant precisely on left cosets of Gx, so [F5] gives a bijection Φ‾x:G/Gx→G⋅x. It is smooth because the submersion charts in [F4] provide local smooth sections s of q and Φ‾x=Φx∘s locally. At eGx, its differential is the map induced by d(Φx)e on g/gx; steps 2.1 and 3.1 make it injective with image im⁡d(Φx)e. Equivariance translates this calculation to every coset, so Φ‾x is an injective immersion and its image carries the canonical immersed-orbit structure.

5.1F2F4F6step 3.1step 4.1∎

Under that structure, step 4.1 gives Tx(G⋅x)=im⁡d(Φx)e={XM(x):X∈g}. The stabilizer is nonempty and may be all of G; then the orbit tangent and quotient are zero. A trivial stabilizer gives kernel zero. Disconnected groups and noneffective actions are allowed. There is no metric, boundary, endpoint, or biconditional. ACω is used through [F2] and [F4], and the pointwise linear algebra adds no choice.

Depends on

Dependency tree · 2 levels

Sources