Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)
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.

Regular elements form a connected dense open subset

Statement

In a complex semisimple Lie algebra g, the set of regular elements is a connected dense Zariski-open subset of g.

Facts & Assumptions

Given: A complex semisimple Lie algebra g of dimension n and rank r.

Proof

technique · direct
1.1givenalgebra

By Regular elements and rank for a complex semisimple Lie algebra, r is the minimum of the dimensions of the centralizers of elements of g. These dimensions belong to the finite set {0,…,n}, and g is nonempty, so the minimum is attained. Thus at least one regular element exists.

2.1step 1.1algebra

In a fixed basis, the matrix entries of ad⁡x depend linearly on x. Rank-nullity gives dim⁡Cg(x)=n−rank⁡(ad⁡x). Hence regularity is the condition that the rank equals its attained maximum n−r. For n−r>0, the nonregular locus is the common zero set of the (n−r)×(n−r) minors. If n−r=0, every element is regular. In either case the regular locus is a nonempty Zariski-open set. A nonzero minor at a regular point remains nonzero on a Euclidean neighborhood; a polynomial vanishing on the regular locus therefore vanishes identically. Thus the regular locus is Zariski dense.

3.1step 2.1algebra∎

Let x,y be regular. On the complex affine line through them, choose a maximal minor nonzero at x (when n−r=0, the whole space is regular). Its restriction is a nonzero one-variable polynomial, so the nonregular points on that line form a finite set. A complex line with finitely many points removed is path connected, giving a path of regular elements from x to y. The zero-dimensional case is a singleton. Thus the regular locus is connected.

Depends on

Used by

Dependency tree · one level

1 result within one dependency step 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