Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Real forms correspond to conjugate-linear involutions

Statement

Let g be a finite-dimensional complex Lie algebra (Real form of a complex Lie algebra). For a real form g0 of g let σg0 be the conjugate-linear map σg0(X+iY):=XiY(X,Yg0), well-defined by the real direct-sum decomposition g=g0ig0. Then:

  1. σg0 is a conjugate-linear involution of g with fixed locus g0, and the assignment g0σg0 is injective.
  2. Conversely, if σ is a conjugate-linear involution of g, then gσ={Z:σZ=Z} is a real form of g, its associated involution σgσ equals σ, and (g0)σg0=g0.
  3. For every complex automorphism u of g one has u(g0)=(g)uσg0u1, and g0=u(g0) if and only if σg0=uσg0u1. Consequently the constructions above induce mutually inverse bijections between isomorphism classes of real forms of g and conjugacy classes of conjugate-linear involutions, and conjugate real forms correspond to conjugate involutions.

Facts & Assumptions

Given: A finite-dimensional complex Lie algebra g; a real form g0 of g with g=g0ig0; a conjugate-linear involution σ of g; and a complex automorphism u of g.

[L1]

The real form condition means that the complex-linear extension e ⁣:g0RCg, e(Xz)=zX, of the inclusion is an isomorphism, equivalently g0ig0=0 and g=g0+ig0, with g0 closed under the bracket; the conjugate-linear involution condition is stated in the same definition (Real form of a complex Lie algebra).

[L2]

For a real Lie algebra h0 with complexification h0RC, the map σ0(Xz)=Xz is a well-defined conjugate-linear bracket-preserving involution with fixed locus h01, and the canonical embedding is an injective real Lie-algebra homomorphism (Complexification has a canonical conjugation with fixed algebra g zero).

Proof technique: direct.

1.1 Every Zg has a unique expression Z=X+iY with X,Yg0 by [L1], so σg0 is well-defined and additive; it is conjugate-linear because σg0((a+ib)(X+iY))=(aXbY)i(bX+aY)=(a+ib)(XiY) for real a,b, and it is involutive with fixed locus exactly g0={X+i0}, since XiY=X+iY forces 2Y=0. If σg0=σg0, then their fixed loci g0,g0 coincide, so the assignment is injective. [L1, algebra]

1.2 For a conjugate-linear involution σ, the fixed locus gσ is a real subspace: it is closed under addition and under real scalars, and if Zgσ with Z0 then iZgσ because σ(iZ)=iσZ=iZiZ; hence gσigσ=0. Every Zg decomposes as Z=12(Z+σZ)+12(ZσZ) with 12(Z+σZ) fixed and 12(ZσZ) anti-fixed, so g=gσigσ. The fixed locus is a real Lie subalgebra because σ[X,Y]=[σX,σY]=[X,Y] for X,Ygσ. [L1, algebra]

2.1 σg0 preserves brackets: writing Z=X+iY, W=U+iV with X,Y,U,Vg0 and using C-bilinearity, [Z,W]=([X,U][Y,V])+i([X,V]+[Y,U]) with both components in the real subalgebra g0 by [L1], so σg0[Z,W]=([X,U][Y,V])i([X,V]+[Y,U])=[XiY,UiV]=[σg0Z,σg0W]. [L1, step 1.1, algebra]

2.2 The involution associated with gσ is σ: since σ is conjugate-linear and fixes X,Ygσ, we have σ(X+iY)=σX+iσY=XiY=σgσ(X+iY) for all X,Ygσ, and by step 1.2 every element of g is of this form. The composite assignments are therefore inverse on the objects displayed: (g0)σg0=g0 by step 1.1 and σgσ=σ by the displayed computation. [step 1.1, step 1.2, algebra]

3.1 Let u be a complex automorphism. For Zg, one has Zu(g0) exactly when u1Zg0, equivalently when σg0u1Z=u1Z, and this is equivalent to uσg0u1Z=Z. Hence u(g0)=guσg0u1. Applying step 2.2 to this involution gives σu(g0)=uσg0u1. Conversely, if σg0=uσg0u1, then their fixed loci give g0=u(g0). [L1, step 1.1, step 1.2, step 2.2, algebra]

4.1 The two constructions are bijective at the level of isomorphism classes. Steps 1.1 and 2.2 first show that they are mutually inverse on objects. If f:g0g0 is an isomorphism of real Lie algebras, let e0:g0RCg and e0:g0RCg be the complex-linear isomorphisms furnished by [L1]. Then u=e0(fidC)e01 is a complex Lie-algebra automorphism of g and carries g0 onto g0. Conversely, a complex automorphism carrying g0 onto g0 restricts to a real Lie-algebra isomorphism of those fixed real subalgebras. Thus ordinary real-isomorphism classes of real forms are exactly the AutC(g)-orbits. Step 3.1 identifies these orbits with conjugacy classes of involutions, proving the asserted class bijection. [L1, step 1.1, step 2.2, step 3.1, algebra] ∎

Depends on

Used by

Dependency tree · two levels

6 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