Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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 sl2

Example

Assume AC (The Axiom of Choice). In sl2(C)=Ch⊕Ce⊕Cf with the root α of Cartan subalgebra and roots of sl2, 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 sl2, and the reflection sα:h∗→h∗ of Root reflection defined by a coroot is −id⁡, because h∗ is one-dimensional and sα(α)=−α. The inner automorphism τα:=Ad⁡eeAd⁡e−fAd⁡ee 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=eee−fee=(01−10)∈SL2(C) sends h↦−h, e↦−f, f↦−e, 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 sl2, The special linear Lie algebra sl2 and Coroot of a Lie-algebra root, together with the reflection sα of Root reflection defined by a coroot.

Verification

technique · direct
1.1givenalgebra

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.

1.2givenalgebra

The element W=eee−fee is the product of the three matrix exponentials ee=(1101), e−f=(10−11), ee=(1101), which multiplies to (01−10); it lies in SL2(C) and satisfies W2=−I, WhW−1=−h.

2.1givenstep 1.2algebra

Define τα=Ad⁡W on the displayed matrix algebra. Since Ad⁡AAd⁡B=Ad⁡AB for invertible matrices, step 1.2 gives τα=Ad⁡eeAd⁡e−fAd⁡ee for the explicitly chosen standard triple. Direct conjugation acts on its basis by h↦−h, e↦−f, f↦−e: indeed WeW−1=(00−10)=−f and WfW−1=(0−100)=−e. Hence τα maps gα=Ce to g−α=Cf and back, and its action on h is −id⁡.

3.1givenstep 1.1step 2.1algebra∎

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 ±α.

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