Chapter 2. Classification of finite reflection groups
FC15 — Humphreys, Reflection Groups and Coxeter Groups.
This chapter contains 13 definitions, 5 theorems, 6 propositions, 1 lemma, 1 corollary, 4 constructions, 1 remark, 1 criterion and 2 other statements.
Nobody has checked this chapter against Lean yet, so the statements below say nothing about whether they are formalized.
Definition: Coxeter graph of a finite reflection group
For simple roots Δ, the Coxeter graph has one vertex per simple reflection, an edge between distinct vertices when m(α,β)>2, labelled by m(α,β) when >3; omitted edges mean m=2 and label 3 is conventionally omitted. It determines W up to abstract isomorphism.
Proposition: geometric uniqueness from the Coxeter graph
If two essential finite reflection groups have the same Coxeter graph, an isometry of their Euclidean spaces identifies compatible simple systems and conjugates the groups. In a common V they are O(V)-conjugate.
Definition: irreducible Coxeter system
A Coxeter system is irreducible when its Coxeter graph is connected; the associated root system is also called irreducible.
Proposition: decomposition by connected Coxeter-graph components
If the Coxeter graph has connected components with vertex sets S_1,…,S_r, then W is the direct product W_{S_1}×⋯×W_{S_r}, and each (W_{S_i},S_i) is irreducible.
Definition: abstract Coxeter graph
A Coxeter graph is a finite undirected graph whose edges are labelled by integers ≥3 or ∞, with label 3 omitted; set m(s,s)=1 and m(s,s′)=2 for nonadjacent distinct vertices.
Construction: bilinear form associated to a Coxeter graph
For vertex set S, associate the symmetric matrix/form with diagonal 1 and off-diagonal entry −cos(π/m(s,s′)), interpreting m=∞ as cos 0=1.
Definition: positive definite, semidefinite, and positive type
A symmetric matrix/form is positive definite when x^tAx>0 for x≠0, positive semidefinite when ≥0, and of positive type when positive semidefinite. A Coxeter graph inherits these adjectives through its associated form.
Criterion: principal-minor criterion for positive type
A symmetric matrix is positive definite iff all leading principal minors are positive; the corresponding nonnegative condition characterizes positive semidefiniteness in the setup used by the source.
Proposition/table: standard connected positive-definite Coxeter graphs
The graphs A_n,B_n,D_n,E_6,E_7,E_8,F_4,H_3,H_4,I_2(m) are positive definite. The source tabulates det(2A): n+1,2,4,3,2,1,1,3−√5,(7−3√5)/2,4sin²(π/m), respectively.
Proposition/table: standard connected positive-semidefinite affine graphs
The extended graphs ilde A_n, ilde B_n, ilde C_n, ilde D_n, ilde E_6, ilde E_7, ilde E_8, ilde F_4, ilde G_2 are positive semidefinite but not positive definite; each is obtained by adjoining one vertex to the corresponding finite graph. The auxiliary graphs Z_4,Z_5 are not of positive type.
Definition: subgraph of a Coxeter graph
A proper subgraph is obtained by deleting vertices/incident edges and/or decreasing edge labels; the graph is then said to contain that subgraph.
Definition: indecomposable symmetric matrix
A real matrix is indecomposable if its index set admits no nontrivial partition I⊔J with all cross-block entries zero. A Coxeter matrix is indecomposable exactly when its graph is connected.
Proposition: Perron–Frobenius/M-matrix lemma
Let A be symmetric, positive semidefinite, indecomposable, with nonpositive off-diagonal entries. Its nullspace has dimension at most one; its least eigenvalue is simple and has an eigenvector with all coordinates strictly positive.
Corollary: proper subgraphs of connected positive-type graphs
Every proper subgraph of a connected Coxeter graph of positive type is positive definite.
Theorem: classification of connected Coxeter graphs of positive type
The connected positive-type Coxeter graphs are exactly the finite positive-definite graphs of Figure 1 and the affine positive-semidefinite graphs of Figure 2.
Definition: crystallographic subgroup
A subgroup G≤GL(V) is crystallographic if it stabilizes a lattice L, the Z-span of a basis of V.
Proposition: edge-label restriction for crystallographic reflection groups
If finite reflection group W is crystallographic, then for distinct simple roots m(α,β)∈{2,3,4,6}.
Definition: crystallographic root system and Cartan integers
A root system is crystallographic if 2(α,β)/(β,β)∈Z for all roots α,β. These integers are Cartan integers. The associated reflection group is its Weyl group.
Theorem/recorded classification: Weyl groups are crystallographic reflection groups
The Weyl groups arising from crystallographic root systems are exactly the finite reflection groups whose Coxeter labels lie in {2,3,4,6}. Distinct root systems B_n,C_n have the same Weyl group.
Definition/result: long and short roots; Dynkin diagram
An irreducible crystallographic root system has at most two root lengths, with squared-length ratio 2 or 3. Multiple Coxeter edges are oriented toward the short root, producing the Dynkin diagram; one-length systems are simply laced.
Definition/construction: coroots and dual root system
For α∈Φ, α∨=2α/(α,α). The set Φ∨ is a crystallographic root system with simple system Δ∨ and the same Weyl group; B_n and C_n are dual.
Definition: root and coroot lattices
The Z-span L(Φ) is the root lattice and L(Φ∨) the coroot lattice; both are W-stable.
Definition: weight and coweight lattices; index of connection
The weight lattice is L^*(Φ)={λ | (λ,α∨)∈Z for all α}, and the coweight lattice analogously uses roots. The root lattice has finite index f in the weight lattice, equal to the determinant of the Cartan matrix; f is the index of connection.
Definition/result: root order and highest roots
Relative to Δ, μ≤λ when λ−μ is a nonnegative integral combination of simple roots. An irreducible root system has a unique highest root (long) and a unique highest short root.
Theorem/result: Weyl orbits by root length
In an irreducible crystallographic root system, all long roots form one W-orbit and all short roots form one W-orbit.
Remark/comparison: nonreduced crystallographic root systems BCn
If the reducedness axiom Φ∩Rα={±α} is dropped, the only new irreducible crystallographic type is BC_n, obtained by superimposing B_n and C_n.
Construction: root systems An,Bn,Cn,Dn
The source gives explicit Euclidean/lattice realizations, simple systems, highest roots, and Weyl-group descriptions for A_n,B_n,C_n,D_n.
Construction: exceptional crystallographic root systems G2,F4,E6,E7,E8
The source gives explicit lattice/vector realizations, bases and highest roots for G_2,F_4,E_6,E_7,E_8, including E_6,E_7 as canonical subsystems of E_8.
Theorem/table: orders and root counts of irreducible Weyl groups
Using orbit–stabilizer on a highest root, the source computes |W| and |Φ| for every irreducible Weyl group: A_n:(n+1)!,n(n+1); B_n/C_n:2^n n!,2n²; D_n:2^{n−1}n!,2n(n−1); E_6:27·34·5,72; E_7:210·34·5·7,126; E_8:214·35·5²·7,240; F_4:2^7·3²,48; G_2:12,12.
Comparison: exceptional Weyl-group realizations
The source records group-theoretic/geometric realizations: W(F_4)=W(D_4)⋊S_3; W(E_6) acts on the 27 lines on a cubic surface with simple rotation subgroup of order 25920; W(E_7),W(E_8) yield orthogonal/symplectic groups over F_2 via root-lattice quotients.
Comparison: noncrystallographic types H3,H4
H_3 is the full reflection symmetry group of the icosahedron/dodecahedron, order 120 with 15 reflections; H_4 is the symmetry group of the 120-cell/600-cell, order 14400 with 60 reflections.
Construction: quaternionic realization of H4 roots
Identify R^4 with the real quaternions. Any finite even-order subgroup of unit quaternions is a root system because reflection in unit α is λ↦−αar λ α. The explicit 120-element quaternion subgroup built from 1,(1+i+j+k)/2 and golden-ratio coordinates gives the H_4 root system and a displayed simple system.
Lemma: finite even-order quaternion subgroup is a root system
Every finite even-order subgroup G of the multiplicative group of real quaternions, viewed as unit vectors in R^4, satisfies the root-system axioms.
Theorem/result: orders of H3 and H4 from the root construction
The 120 quaternion roots form one W-orbit; the stabilizer of a suitable root is the H_3 subgroup of order 120. Hence |W(H_4)|=120²=14400 and the induced H_3 order is 120.