Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

The Weyl reflection in sl_2

Example

Assume AC (The Axiom of Choice). In sl2(C)=ChCeCf with the root α of Cartan subalgebra and roots of sl_2, the coroot is hα=h. Choose the standard root triple (eα,fα,hα)=(e,f,h), whose bracket relations are the displayed matrix relations of The special linear Lie algebra sl_2, and the reflection sα:hh of Root reflection defined by a coroot is id, because h is one-dimensional and sα(α)=α. The inner automorphism τα:=AdeeAdefAdee is the standard-matrix specialization of the construction in Root reflections are induced by inner automorphisms and realizes the reflection directly: τα acts on h as 1, fixing only 0=kerα, and conjugation by the matrix W=eeefee=(0110)SL2(C) sends hh, ef, fe, hence interchanges the two roots ±α.

Facts & Assumptions

Given: AC; the algebra sl2(C) with its root α, standard matrices (e,f,h), standard root triple (eα,fα,hα)=(e,f,h), and coroot hα=h as in Cartan subalgebra and roots of sl_2, The special linear Lie algebra sl_2 and Coroot of a Lie-algebra root, together with the reflection sα of Root reflection defined by a coroot.

Verification

technique · direct
1.1

Since h=Ch is one-dimensional, so is h; it is spanned by α with α(h)=2. The reflection formula gives sα(α)=αα(hα)α=α2α=α, so sα=id on the whole line.

givenalgebra
1.2

The element W=eeefee is the product of the three matrix exponentials ee=(1101), ef=(1011), ee=(1101), which multiplies to (0110); it lies in SL2(C) and satisfies W2=I, WhW1=h.

givenalgebra
2.1

Define τα=AdW on the displayed matrix algebra. Since AdAAdB=AdAB for invertible matrices, step 1.2 gives τα=AdeeAdefAdee for the explicitly chosen standard triple. Direct conjugation acts on its basis by hh, ef, fe: indeed WeW1=(0010)=f and WfW1=(0100)=e. Hence τα maps gα=Ce to gα=Cf and back, and its action on h is id.

givenstep 1.2algebra
3.1

Since τα acts on h as 1, its induced action on h is also 1: for λh the induced functional is λτα1=λ(id)=λ. This equals sα by step 1.1, so the Weyl reflection of the root α is realized by the inner automorphism τα and swaps the roots ±α.

givenstep 1.1step 2.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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