LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-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.

The sign of the Weyl length is multiplicative

Statement

Let $W$ be the Weyl group of the root system $Φ$ with its real span $E = {span}_{R} Φ$ and length function $ℓ$ (Finite Weyl root system, lattice and chamber conventions, Root reflections and the Weyl group action). Then $(- 1)^{ℓ (u v)} = (- 1)^{ℓ (u)} (- 1)^{ℓ (v)} (u, v \in W),$ so that $w \mapsto (- 1)^{ℓ (w)}$ is a group homomorphism $W \to {\pm 1}$ , and this homomorphism is the determinant of the action of $W$ on $E$ : $(- 1)^{ℓ (w)} = \det (w)$ for every $w \in W$ . In particular $(- 1)^{ℓ (w^{- 1})} = (- 1)^{ℓ (w)}$ .

Facts & Assumptions

Given: The finite root system $Φ$ spanning the real vector space $E$ of dimension $n$ with its positive definite form, the Weyl group $W$ generated by the root reflections $s_{α}$ , its simple reflections $s_{i}$ and the length function $ℓ$ , and elements $u, v, w \in W$ .

[F1]

For each root $α$ the reflection $s_{α} (λ) = λ - ⟨ λ, α^{\lor} ⟩ α$ fixes $α^{⊥}$ pointwise and sends $α$ to $- α$ ; in particular $E = R α \oplus α^{⊥}$ and $α \land e_{2} \land \dots \land e_{n}$ is a nonzero element of $Λ^{n} E$ for a basis $e_{2}, \dots, e_{n}$ of $α^{⊥}$ (Root reflections and the Weyl group action, Finite Weyl root system, lattice and chamber conventions).

[F2]

If $T : V \to V$ is an endomorphism of an $n$ -dimensional vector space, then $Λ^{n} T = \det (T) \cdot {id}_{Λ^{n} V}$ on the one-dimensional space $Λ^{n} V$ ; and $\det (S \circ T) = \det (S) \det (T)$ for endomorphisms $S, T$ (On $Λ^{n} V$ , the induced map $Λ^{n} T$ is multiplication by $\det T$ , Determinant multiplicativity follows from the top exterior power).

[F3]

The simple reflections generate $W$ and $ℓ (w)$ is the least number of simple reflections in an expression for $w$ ; every simple reflection $s_{i}$ is a root reflection and $ℓ (s_{i}) = 1$ ; all of this includes the case $Φ = \emptyset$ , where $E = 0$ and $W = {1}$ (Finite Weyl positive roots and simple reflections, Finite Weyl root system, lattice and chamber conventions, Weyl length equals inversion number).

Proof

technique · direct

1.1F1F2algebra

If $E = 0$ , then $W = {1}$ and both the length sign and the determinant of its identity are $1$ , so all assertions hold. Assume $\dim E \geq 1$ . For every root $α$ one has $\det (s_{α}) = - 1$ : choosing the basis $(α, e_{2}, \dots, e_{n})$ of $E$ with $e_{2}, \dots, e_{n}$ a basis of $α^{⊥}$ , [F1] gives $s_{α} (α) = - α$ and $s_{α} (e_{i}) = e_{i}$ , so $Λ^{n} s_{α} (α \land e_{2} \land \dots \land e_{n}) = (- α) \land e_{2} \land \dots \land e_{n} = - (α \land e_{2} \land \dots \land e_{n})$ , and since this wedge is a basis of the one-dimensional space $Λ^{n} E$ , [F2] forces $\det (s_{α}) = - 1$ .

2.1F2F3step 1.1algebra

Every $w \in W$ is a product of simple reflections by [F3]; if $w = s_{i_{1}} \dots s_{i_{k}}$ is any such expression, then repeated use of [F2] together with step 1.1 gives $\det (w) = \prod_{j = 1}^{k} \det (s_{i_{j}}) = (- 1)^{k}$ , so $\det (w)$ agrees with $(- 1)^{k}$ for every expression of $w$ ; choosing an expression of minimal length $k = ℓ (w)$ , which exists by [F3], gives $\det (w) = (- 1)^{ℓ (w)}$ .

3.1F2step 2.1algebra∎

For $u, v \in W$ the multiplicativity in [F2] and step 2.1 give $(- 1)^{ℓ (u v)} = \det (u v) = \det (u) \det (v) = (- 1)^{ℓ (u)} (- 1)^{ℓ (v)}$ , so $w \mapsto (- 1)^{ℓ (w)}$ is a homomorphism $W \to {\pm 1}$ agreeing with the determinant; applying it to $w^{- 1}$ and using $\det (w)^{- 1} = \det (w) \in {\pm 1}$ gives $(- 1)^{ℓ (w^{- 1})} = \det (w^{- 1}) = \det (w) = (- 1)^{ℓ (w)}$ .

Depends on

Used by

The Racah--Speiser tensor-product algorithm Corollary
The Weyl alternation operator Definition
Regularized evaluation of the Weyl character quotient at one Lemma
Weyl alternants are skew-invariant Lemma
Steinberg's tensor-product multiplicity formula Theorem

Dependency tree · two levels

15 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

P. Etingof, Lie Groups and Lie Algebras II (MIT 18.755, Spring 2024), complete lectures (standard reference, not scraped)
A. W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)