Alphabeta Math
PropositionStatement: 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.

Classical real forms of the classical complex lie algebras

Statement

Assume the Axiom of Choice. Let g be a complex simple Lie algebra of classical type An (n1), Bn (n2), Cn (n3) or Dn (n4), realized as sln+1(C), so2n+1(C), sp2n(C) or so2n(C) (Classical types correspond to sl, so and sp, Classical complex matrix Lie algebras). Then, up to isomorphism and up to the admissible ranges and low-rank coincidences stated below, the real forms of g are:

  1. for An: sln+1(R) and su(p,q) with p+q=n+1, pq0; and su(2m)=slm(H) with n+1=2m;
  2. for Bn: so(p,q) with p+q=2n+1, pq0;
  3. for Cn: sp2n(R) and sp(p,q) with p+q=n, pq0;
  4. for Dn: so(p,q) with p+q=2n, pq0, and so(2n).

The compact form occurs in each list at the signature q=0, and the split form is sln+1(R) for type An, so(n+1,n) for Bn, sp2n(R) for Cn and so(n,n) for Dn; within the inner families su(p,q) and sp(p,q) the real rank min(p,q) is maximal exactly when pq1 (for type An the corresponding painted root is the middle one). Among the low-rank coincidences are sl2so3sp2, sp4so5, so4sl2sl2, so6sl4, together with su(1,1)sl2(R), so(2,1)su(1,1), sp4(R)so(3,2), sp(2)so(5), sp(1,1)so(4,1), so(4)su(2)su(1,1) and so(6)su(3,1), together with the duplicate so(8)so(6,2) in the type-D4 list.

Facts & Assumptions

Given: The Axiom of Choice; the classical complex matrix Lie algebras of Classical complex matrix Lie algebras with their types as in Classical types correspond to sl, so and sp; and the correspondence between real forms and conjugate-linear involutions of Real forms correspond to conjugate-linear involutions.

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the classification theorem of [L3]. The explicit finite matrix constructions in steps 1.1 and 2.1 make no additional choice.

[L1]

A real Lie subalgebra g0 of a complex Lie algebra g is a real form if and only if it is the fixed locus of a conjugate-linear involution of g (Real forms correspond to conjugate-linear involutions, Real form of a complex Lie algebra).

[L2]

The complex matrix algebras slm(C), som(C) and sp2n(C) and their classical types are fixed by Classical complex matrix Lie algebras and Classical types correspond to sl, so and sp. A complex change of basis between two nondegenerate complex symmetric or alternating forms gives an isomorphic complex orthogonal or symplectic algebra, so Euclidean matrix models may be used to display conjugations.

[L3]

Knapp's classification theorem and its tables identify the real forms of the four classical types with exactly the matrix families in the Statement, in the stated range normalization (Source, Figure 6.1 and Theorem 6.105(c), printed pp. 413--415 and 421--422). Etingof obtains the same families directly from the inner classes of An,Bn,Cn,Dn (Source, Lecture 40, §40.3, printed pp. 188--189). This is the classical specialization of Classification of real semisimple lie algebras.

[L4]

The compact form is characterized by negative-definite Killing form and the split form by a split Cartan subalgebra (Compact real form of a complex semisimple Lie algebra, Split real form). Knapp's restricted-root computation gives real rank min(p,q) for su(p,q) and sp(p,q) and the source's table (6.110) records the stated real low-rank coincidences (printed pp. 422--426). The complex low-rank coincidences are those of [L2].

Proof

technique · direct
1.1

Put Sp,q=diag(Ip,Iq) and Jr=(0IrIr0). In the Euclidean orthogonal model, and in the standard symplectic model with form Jn, the following are well-typed conjugate-linear involutive automorphisms: complex algebraconjugationslm(C)X,Sp,qXSp,q,JrXJr1 (m=2r),som(C)Sp,qXSp,q,sp2n(C)X,Hp,qXHp,q,Hp,q=diag(Sp,q,Sp,q),so2n(C)JnXJn1. The displayed matrices have respectively sizes m, m, 2n and 2n; in particular the last Jn is 2n by 2n, with no odd-dimensional completion. Direct substitution in the defining symmetric or alternating form shows that each map preserves its complex algebra and squares to the identity.

L2algebra
2.1

The fixed loci in step 1.1 are respectively slm(R), su(p,q), su(2r)=slr(H), so(p,q), sp2n(R), sp(p,q) and so(2n). For the orthogonal signature form, conjugation by D=diag(Ip,iIq) identifies the fixed locus in the Euclidean skew-symmetric model with {AMm(R):ATSp,q+Sp,qA=0}. By [L1] every fixed locus is therefore a real form of the indicated complex algebra.

L1step 1.1algebra
3.1

The type-by-type classification [L3] says that the fixed loci of step 2.1 exhaust the real forms: type An has the real, Hermitian-signature and, when n+1 is even, quaternionic forms; types Bn and Dn have the orthogonal signatures, with Dn also having so(2n); and type Cn has the real symplectic and quaternionic-Hermitian forms. Thus no additional real-form class is missing.

A1L3step 2.1
3.2

Exchanging the positive and negative blocks gives su(p,q)su(q,p), so(p,q)so(q,p) and sp(p,q)sp(q,p). The compact classes are the q=0 members by [L4]. The real diagonal Cartan subalgebras show that sln+1(R), sp2n(R) and so(n,n) are split, and the orthogonal form of signature (n+1,n) is split in type Bn.

L4step 2.1algebra
4.1

The restricted-root computation in [L4] gives real rank min(p,q) for su(p,q) and sp(p,q), so within either signature family it is maximal exactly when pq1. The same source table supplies the real low-rank coincidences in the Statement, while the complex coincidences are those of [L2]. These identifications account for the admissible-range repetitions and do not remove any class from step 3.1.

L2L4step 3.1
5.1

Steps 2.1 and 3.1 prove occurrence and exhaustion, step 3.2 identifies the compact and split members, and step 4.1 supplies the rank and low-rank clauses. Hence the displayed families are exactly the real forms of the four classical complex simple types, with the asserted normalization.

step 2.1step 3.1step 3.2step 4.1

Remarks

Exhaustion. Every real form is accounted for by the classification theorem's enumeration of the real forms of the type, together with the source's identification of the classical entries with the matrix algebras su(p,q), so(p,q), sp(p,q), sp2n(R), so(2n), sln(R) and sln(H) (Knapp, Figure 6.1 of the source, printed pp. 413-415, and tables (6.107) and (6.110), printed pp. 424 and 426). The constructions of the proof exhibits each entry independently as the fixed locus of a conjugate-linear involution.

What is proved here. Every family is exhibited by a dimensionally correct conjugate-linear involution (in particular the so(2n) operator uses the 2n by 2n matrix Jn), and the classification theorem supplies exhaustion. The compact, split, real-rank and low-rank clauses are then read with the exact range conventions of the cited tables.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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