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.

✓ 11 results · all verified · 11 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; all 11 also cleared it.

Lie Subgroups, Actions, and Homogeneous Spaces — Examples

1 · Prerequisites

2 · Summary

These examples separate immersed subgroups from embedded ones, identify classical homogeneous spaces, and compute two associated bundles. They also show independently why properness and freeness are both necessary for the principal-bundle quotient theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

An irrational line as a dense immersed Lie subgroup of a torus

Example

Assume ACω and fix α∈R∖Q. Then

i:R⟶T2,i(t)=(e2πit,e2πiαt)

identifies R with a one-dimensional immersed Lie subgroup whose image is dense, proper, nonclosed, and nonembedded in T2.

Facts & Assumptions

Given: ACω, an irrational real number α, and the displayed winding homomorphism i.

[A1]

The winding map is an injective immersion and homomorphism, and its image is dense. The irrational torus flow is free with dense orbits.

[A2]

The homomorphism-image theorem equips its image with the unique intrinsic immersed-subgroup structure for which the corestriction is a submersion. The Axiom of Countable Choice (ACω), Images are immersed Lie subgroups.

[F1]

Embeddedness means that this intrinsic topology agrees with the ambient subspace topology. Immersed, embedded, and closed Lie subgroups.

Verification

technique · calculate the image and compare its intrinsic and ambient topologies
1.1A1A2

By [A1], i is an injective immersed homomorphism with dense image. Since its kernel is trivial, the canonical image structure in [A2] is transported from the one-dimensional source R.

1.2A1algebra

The image is proper. The point (1,eπiα) is not in it: equality of the first coordinate would force t=n∈Z, while equality of the second would make α(n−12) an integer, impossible because a nonzero rational multiple of irrational α is irrational. A proper dense subset is not closed.

2.1A1A2F1step 1.1algebra∎

For each j≥1, let qj be the least positive integer satisfying ∥qjα∥<1/j, whose existence is the finite-pigeonhole calculation in [A1]. Irrationality makes every fixed ∥qα∥ positive, so qj→∞. Nevertheless i(qj)=(1,e2πiαqj)→(1,1)=i(0) in the ambient subspace. Hence the inverse of i on its image is not continuous, so [F1] shows that the subgroup is not embedded. Leastness makes the sequence choice-free; ACω is inherited only through the general image supplier [A2]. The source dimension is exactly one, its tangent (1,α) is nonzero, and no endpoint is present.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

SL(n) as a closed Lie subgroup of GL(n)

Example

Assume ACω, let F be R or C, and let n≥1. Then

SL⁡n(F)=ker⁡(det⁡:GL⁡n(F)→F×)

is a closed embedded normal Lie subgroup, and

Lie⁡(SL⁡n(F))=sln(F)={X∈Mn(F):tr⁡X=0}.

Facts & Assumptions

Given: ACω, F∈{R,C}, and an integer n≥1.

[F1]

A Lie group has smooth multiplication and inversion; determinant and trace have their finite Leibniz and diagonal-sum formulas. Lie group, For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix, The trace of a square matrix over a commutative ring.

[A1]

The kernel of a smooth Lie-group homomorphism is closed, embedded and normal, with tangent algebra equal to the kernel of its identity differential. The Axiom of Countable Choice (ACω), Kernels are closed embedded normal Lie subgroups.

[F2]

A regular level has tangent space equal to the kernel of its differential. The tangent space of a regular level set is the kernel.

Verification

technique · compute the determinant differential at the identity
1.1F1A1algebra

The locus det⁡≠0 is open in the finite-dimensional real vector space underlying Mn(F). Matrix multiplication is polynomial there, and the adjugate formula A−1=adj⁡(A)/det⁡A makes inversion smooth, so this locus is the Lie group GL⁡n(F) in the sense of [F1]. The determinant is polynomial, hence smooth, and multiplicativity makes det⁡:GL⁡n(F)→F× a Lie-group homomorphism. Its identity fibre is exactly SL⁡n(F), so [A1] makes this fibre a closed embedded normal Lie subgroup.

1.2F1F2algebra

In the Leibniz expansion of det⁡(I+tX), the identity permutation contributes 1+t∑iXii+O(t2), while every nonidentity permutation needs at least two off-diagonal factors and contributes O(t2). Thus d(det⁡)I(X)=tr⁡X. This differential is onto F: the matrix diag⁡(z,0,…,0) has trace z. Left multiplication transports surjectivity to every point of the identity fibre, so the fibre is regular and [F2] gives the same tangent kernel.

2.1A1F1F2step 1.1step 1.2∎

Combining steps 1.1 and 1.2 with [A1] yields Lie⁡(SL⁡n(F))=ker⁡d(det⁡)I={X:tr⁡X=0}. For n=1 the subgroup and Lie algebra are both trivial; singular matrices X are allowed as tangent vectors. The complex case is read as a real Lie group, and the complex-linear trace map is also onto as a real map. No endpoint or metric choice occurs. ACω is inherited exactly through [A1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The kernel and image of the determinant homomorphism

Example

Assume ACω and n≥1. For real matrices,

det⁡:GLn(R)→R×

has kernel SLn(R) and image R×. On GLn+(R)={A:det⁡A>0} its image is R>0. Hence the first-isomorphism factorization identifies the corresponding intrinsic quotients with these image Lie groups.

Facts & Assumptions

Given: ACω and an integer n≥1.

[A1]

A smooth Lie-group homomorphism factors through its canonical immersed image as a surjective submersion followed by inclusion. The Axiom of Countable Choice (ACω), First-isomorphism factorization for Lie group homomorphisms.

Verification

technique · compute kernel and image explicitly
1.1F1algebra

Multiplicativity in [F1] and polynomiality make determinant a smooth Lie-group homomorphism. By definition, its identity fibre is {A:det⁡A=1}=SLn(R).

1.2F1algebra

For each r∈R×, the diagonal matrix diag⁡(r,1,…,1) is invertible and has determinant r. Thus the image on GLn(R) is all of R×. The same matrix lies in GLn+(R) exactly when r>0, so the restricted image is R>0.

2.1A1step 1.1step 1.2∎

Apply [A1]. It gives surjective submersions GLn(R)→R×,GLn+(R)→R>0 with fibres the left cosets of SLn(R), followed in each case by the evident inclusion of the image. Equivalently, the canonical intrinsic quotient by the kernel is isomorphic to the displayed image Lie group. For n=1 these maps are the identity on R× and its positive subgroup. The disconnected two-component image in the first case is intentional. Countable choice is used only through [A1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Spheres as SO(n+1)/SO(n)

Example

Assume ACω. For every n≥1, the standard action gives a canonical SO(n+1)-equivariant diffeomorphism

SO(n+1)/SO(n)≅Sn.

Here SO(n) is embedded as diag⁡(A,1).

Facts & Assumptions

Given: ACω, n≥1, and the standard linear action of SO(n+1) on the unit sphere Sn⊆Rn+1.

[A1]

A transitive smooth action identifies the manifold equivariantly with the quotient by a point stabilizer. The Axiom of Countable Choice (ACω), Transitive smooth actions identify M with G/H.

Verification

technique · prove transitivity and compute the stabilizer
1.1givenalgebra

The action is smooth and preserves Sn. Given u,v∈Sn, extend each to an oriented orthonormal basis whose last vector is respectively u and v; when necessary, changing the sign of one of the first n vectors corrects the orientation. The linear map carrying the first oriented basis to the second is in SO(n+1) and sends u to v. Thus the action is transitive.

1.2givenalgebra

A matrix in SO(n+1) fixes en+1 exactly when it preserves en+1⊥ and has block form diag⁡(A,1). Orthogonality and determinant one then say precisely A∈SO(n). Hence the stabilizer is the displayed copy of SO(n).

2.1A1step 1.1step 1.2∎

Apply [A1] at en+1. The map gSO(n)↦gen+1 is the asserted equivariant diffeomorphism. For n=1, SO(1)={1} and the quotient is SO(2)≅S1. The excluded value n=0 also has the analogous point quotient if one adopts SO(0)=SO(1)={1}, but it is not needed for the stated family. Countable choice is used through [A1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Real and complex projective spaces as homogeneous spaces

Example

Assume ACω. With their standard smooth structures,

RPn≅SO(n+1)/S(O(1)×O(n)),

CPn≅U(n+1)/(U(1)×U(n))

equivariantly and diffeomorphically for n≥1.

Facts & Assumptions

Given: ACω, n≥1, and the natural actions on real and complex lines.

[A1]

A transitive smooth action identifies the manifold with the quotient by a stabilizer. The Axiom of Countable Choice (ACω), Transitive smooth actions identify M with G/H.

Verification

technique · use adapted orthonormal bases and compute block stabilizers
1.1givenalgebra

The actions on lines are smooth: in an affine projective chart where one coordinate is nonzero, the transformed line coordinates are ratios of linear functions with a nonvanishing denominator. Given two real lines, choose unit generators and extend them to oriented orthonormal bases; the resulting element of SO(n+1) carries one line to the other. Given two complex lines, extend unit generators to unitary bases; the resulting element of U(n+1) does the same. Hence both actions are transitive.

1.2givenalgebra

The stabilizer in SO(n+1) of the line Re0 preserves its orthogonal complement and is therefore S(O(1)×O(n))={diag⁡(ε,A):ε=±1, A∈O(n), εdet⁡A=1}. Conversely every such block matrix fixes the line. The stabilizer in U(n+1) of Ce0 is exactly the block subgroup U(1)×U(n): unitarity forces preservation of the orthogonal complement, and every such block matrix fixes the line.

2.1A1step 1.1step 1.2∎

Apply [A1] to the base lines. It yields the two displayed equivariant diffeomorphisms. The determinant-one condition in the real stabilizer is essential; replacing it by O(1)×O(n) would not be a subgroup of SO(n+1). For n=0, both projective spaces are a point and the analogous quotient is trivial. Countable choice is used through [A1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Grassmannians and flag manifolds as homogeneous spaces

Example

Assume ACω. For 0≤k≤n,

Gr⁡k(Rn)≅O(n)/(O(k)×O(n−k)),

Gr⁡k(Cn)≅U(n)/(U(k)×U(n−k)).

More generally, if positive block sizes n1,…,ns sum to n, the corresponding complete or partial real and complex flag manifolds are

O(n)/(O(n1)×⋯×O(ns)),

U(n)/(U(n1)×⋯×U(ns)),

as smooth homogeneous spaces.

Facts & Assumptions

Given: ACω, the standard inner products on Rn and Cn, and the indicated Grassmannians and flag manifolds with their standard smooth structures.

[A1]

A smooth transitive action of a Lie group identifies the manifold with the quotient by the stabilizer. The Axiom of Countable Choice (ACω), Transitive smooth actions identify M with G/H.

Verification

technique · choose adapted orthonormal bases and read off block stabilizers
1.1givenalgebra

Given two k-planes, choose orthonormal bases for each and extend them to orthonormal bases of the ambient space. The orthogonal or unitary map between the adapted bases carries one plane to the other, proving transitivity. The stabilizer of the coordinate k-plane preserves it and its orthogonal complement, hence is exactly the block diagonal subgroup O(k)×O(n−k) or U(k)×U(n−k). Conversely every such block matrix stabilizes the plane.

1.2givenalgebra

For a flag with successive quotient dimensions n1,…,ns, choose an orthonormal basis adapted to all members of the flag. Mapping one adapted basis to another proves transitivity. A unitary or orthogonal transformation fixes the coordinate flag exactly when it preserves each successive orthogonal block, which gives the stated product block subgroup. These actions are smooth in the usual graph-coordinate charts for subspaces.

2.1A1step 1.1step 1.2∎

Apply [A1] to steps 1.1 and 1.2. This gives all displayed equivariant diffeomorphisms. The cases k=0 or k=n have stabilizer the whole group and quotient a point. Repeated or zero flag blocks are omitted because they do not change a flag; partial flags correspond to any positive composition of n. Countable choice is used through [A1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The Möbius line bundle as an associated bundle

Example

For the principal {±1}-bundle p:S1→S1, p(z)=z2, and the sign representation on R, the associated line bundle is the Möbius line bundle.

Facts & Assumptions

Given: The right action z⋅ε=zε of H={±1} on S1, and the representation ρ(ε)t=εt on R.

[F1]

A principal bundle is locally equivariantly a product with its structure group. Principal g bundle and associated fiber bundle.

[F2]

For a right principal bundle and a left representation, the associated relation is [ph,v]=[p,ρ(h)v], and the quotient has its canonical smooth vector-bundle structure. Associated bundles, Associated vector bundles are well-defined.

Verification

technique · identify the quotient relation and its transition sign
1.1F1algebraconstruct

Put U0=S1∖{−1} and U1=S1∖{1}. For −π<θ<π define s0(eiθ)=eiθ/2, and for 0<θ<2π define s1(eiθ)=eiθ/2. These are smooth and satisfy sj(w)2=w. The fibres of p(z)=z2 are exactly {z,−z}, so τj:Uj×H→p−1(Uj), τj(w,ε)=sj(w)ε, is an equivariant bijection with smooth inverse z↦(z2,sj(z2)−1z). Its second component takes values in the discrete zero-dimensional Lie group H, hence is locally constant and smooth. Thus the two τj are principal charts and p is a smooth principal H-bundle in the sense of [F1].

2.1F2step 1.1algebra

The associated relation from [F2] is (z,t)∼(−z,−t), so E=(S1×R)/∼ is a smooth real line bundle over the base circle, with [z,t]↦z2. On the upper component of U0∩U1, the two sections in step 1.1 agree. On the lower component, expressing the same angle in the second interval adds 2π, so s1=−s0 and the associated fibre coordinate changes by ρ(−1)=−1. Thus its transition function is +1 on one overlap component and −1 on the other.

3.1step 1.1step 2.1∎

Writing z=eπix identifies E with ([0,1]×R)/((0,t)∼(1,−t)), because the only two representatives in this half-circle fundamental domain are (0,t) and (1,−t). This is exactly the standard half-twisted-strip Möbius line bundle, and step 2.1 also records its nontrivial sign transition rather than merely the topology of the total space. The zero section and zero fibre vectors are fixed; the two-chart construction uses no choice principle.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Integer translations on the line

Example

Give Z its discrete zero-dimensional Lie-group structure and let it act smoothly on R by

n⋅x=x+n.

This action is free and proper. Its orbit quotient is diffeomorphic to S1, and, under that identification, the orbit map is the principal Z-bundle

p:R⟶S1,p(x)=e2πix.

Facts & Assumptions

Given: The discrete Lie group Z, the usual smooth line R, and the displayed translation action.

[F1]

Any countable discrete group is a zero-dimensional Lie group. Lie group.

[F3]

A smooth free proper left action makes its orbit projection, for the equivalent right action x⋅n=(−n)⋅x=x−n, a principal bundle. Free and proper Lie-group actions, A free proper action makes M to M/G a principal bundle.

Verification

technique · direct
1.1givenF1algebra

Addition gives 0⋅x=x and (m+n)⋅x=m⋅(n⋅x), so the formula is a left action. It is smooth because its restriction to every open component {n}×R is the smooth translation x↦x+n. If n⋅x=x, then n=0, so the action is free.

2.1F2step 1.1

The action is proper. Let K⊆R2 be compact and write Θ(n,x)=(x+n,x). The continuous coordinate projections and difference map (a,b)↦a−b send K to compact, hence bounded, subsets P and D of R by [F2]. Thus the first coordinate of every (n,x)∈Θ−1(K) lies in the finite set E=Z∩D, while x∈P. The set E is finite and therefore compact; hence E×P is compact by [F2]. Because compact K is closed and Θ is continuous, Θ−1(K) is closed in Z×R, and consequently is a closed subspace of the compact set E×P. It is compact by [F2], proving properness.

3.1step 1.1step 2.1algebra

The map p(x)=e2πix is constant on translation orbits. Conversely, p(x)=p(y) exactly when x−y∈Z, so it induces a bijection pˉ:R/Z→S1. For every z0=e2πix0, the restriction of p to (x0−12,x0+12) maps each sufficiently short subinterval diffeomorphically onto an open arc about z0, with a smooth argument branch as inverse. These local inverse branches show that p is a covering map and, using the quotient slice charts supplied by the free proper action, that pˉ and pˉ−1 are smooth. Thus pˉ is a diffeomorphism.

4.1F3step 2.1step 3.1∎

By [F3], the orbit projection R→R/Z is a principal Z-bundle for the right action x⋅n=x−n. Transporting its base along the diffeomorphism pˉ from step 3.1 gives precisely p:R→S1. This verifies every claim, including both the quotient smooth structure and the principal-bundle assertion, without any choice principle.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A free irrational torus action that is not proper

Statement refuted

False claim: every smooth free action of a Lie group on a manifold is proper and has a Hausdorff orbit quotient.

Facts & Assumptions

Given: An irrational number α and T2=S1×S1 with its usual smooth structure.

[F1]

A left action is free when all stabilizers are trivial, and it is proper when (t,x)↦(t⋅x,x) has compact inverse images of compact sets. Free and proper Lie-group actions.

[F2]

For irrational α, the displayed action is smooth and free and all its orbits are dense. The irrational torus flow is free with dense orbits.

[F3]

The wrap-metric circle T=[0,1) is compact, and finite products of compact spaces are compact. The unit-interval circle is a nonempty compact metric space, A product of finitely many compact spaces is compact in the product topology.

Counterexample

technique · constructive
1.1givenF1F2construct

Define the R-action on T2 by t⋅(z,w)=(e2πitz,e2πiαtw). By [F2], it is a smooth free left action.

2.1F2step 1.1

Every orbit is dense by [F2].

2.2F1F3F4step 1.1

The action is not proper. The map u↦e2πiu identifies the wrap-metric circle in [F3] with the complex unit circle S1: their chordal distance is ∣e2πiu−e2πiv∣=2sin⁡(πd(u,v)), so the map is a homeomorphism. Thus [F3] makes S1, then T2×T2, compact. The full inverse image of this compact target under the action-graph map is R×T2. Were it compact, its continuous projection onto R would make R compact by [F4], contrary to the open cover {(−n,n):n≥1}, which has no finite subcover.

3.1F1step 2.1step 2.2discharge-construct: counterexample complete∎

The quotient is not Hausdorff. Each orbit is a proper dense subset: it is dense by step 2.1. For a point (z,w), choose θ∈R with z=e2πiθ. Its orbit meets {1}×S1 only at the countable set {(1,e2πiα(n−θ)w):n∈Z}, so it cannot contain the whole circle {1}×S1 and is therefore proper. If the quotient were Hausdorff, a singleton orbit class would be closed and its inverse image under the quotient map would be a closed orbit, contradicting density and properness. This free, nonproper action therefore refutes both conclusions, without using any choice principle.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A proper nonfree action is not a principal bundle

Statement refuted

False claim: every smooth proper Lie-group action makes its orbit projection a principal bundle for that action.

Facts & Assumptions

Given: The standard rotation action of SO(2) on R2.

[F1]

Every continuous action of a compact Lie group on a manifold is proper. Compact Lie-group actions are proper.

[F2]

Freeness means that every stabilizer is trivial. Free and proper Lie-group actions.

[F3]

The group action in a principal bundle is free and transitive on every fibre. Principal g bundle and associated fiber bundle.

Counterexample

technique · constructive
1.1givenF1construct

Let SO(2) act on R2 by matrix multiplication. This is a smooth action, and SO(2) is compact, so [F1] makes the action proper.

2.1F2step 1.1

Every rotation fixes the origin. Thus the stabilizer of 0 is all of SO(2) rather than the trivial group, and the action is not free by [F2].

3.1F3step 1.1step 2.1discharge-construct: counterexample complete∎

If the orbit projection R2→R2/SO(2) were a principal SO(2)-bundle for this action (or for the equivalent right action x⋅g=g−1x), [F3] would make the action free on the fibre over the orbit of 0. Step 2.1 contradicts this. Hence properness without freeness does not yield a principal bundle. No choice principle is used.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The tangent bundle of G/H as an associated bundle

Example

Assume ACω. If H≤G is closed and acts on g/h by h⋅(X+h)=Ad⁡hX+h, then there is a canonical vector-bundle isomorphism

G×H(g/h)≅T(G/H).

Facts & Assumptions

Given: ACω, a closed subgroup H≤G, and the principal right H-bundle q:G→G/H.

[A1]

The associated quotient uses the relation [gh,v]=[g,Ad⁡hv], has its canonical vector-bundle structure, and q is a smooth principal bundle. The Axiom of Countable Choice (ACω), Associated bundles, Associated vector bundles are well-defined, G to G/H is a smooth principal H-bundle.

[F1]

The map dqe‾:g/h→TeH(G/H) is an isomorphism, and the isotropy differential corresponds to Ad⁡h modulo h. Tangent space of a homogeneous quotient, The isotropy action on G/H is induced by Ad modulo h.

Verification

technique · translate the tangent identification at the identity coset
1.1A1F1algebra

Define Θ([g,X+h])=d(LgG/H)eH(dqe‾(X+h)). This vector lies over gH. The formula is representative-independent. Indeed, [gh,v]=[g,Ad⁡hv] in the associated bundle, while [F1] gives d(Lgh)eHdqe‾(v)=d(Lg)eHd(Lh)eHdqe‾(v)=d(Lg)eHdqe‾(Ad⁡hv).

2.1A1F1step 1.1

On the fibre over gH, Θ is the composite of the linear isomorphisms dqe‾ and d(Lg)eH, so it is a fibrewise-linear bijection. In a principal trivialization with smooth section s:U→G, its coordinate expression is (x,v)⟼d(Ls(x))eHdqe‾(v). This is smooth. Its inverse applies d(Ls(x)−1)x and then dqe‾−1, so it is smooth as well.

3.1A1F1step 2.1∎

Hence Θ is a smooth vector-bundle isomorphism over G/H. If H=G, both sides are the zero bundle over a point; if H={e}, this is the standard left trivialization G×g≅TG. Normality of H is not needed; it is precisely the isotropy action, not an action assumed trivial, that makes step 1.1 work. Countable choice is inherited through [A1] and [F1].

Sources