Signs of geometric roots and faithfulness of the geometric representation

Let cs : CoxeterSystem M W be a Coxeter system with arbitrary index set I, acting on the free real vector space I →₀ ℝ through its standard geometric representation ρ. A vector is called positive when it has nonnegative coefficients and is nonzero, which is exactly Mathlib's strict order 0 < v on finitely supported functions; a vector is negative when v < 0.

The geometric sign criterion says that the sign of the root ρ(w) αᵢ records the length function of W:

• 0 < ρ(w) αᵢ exactly when i is not a right descent of w, that is, ℓ(w sᵢ) = ℓ(w) + 1;
• ρ(w) αᵢ < 0 exactly when i is a right descent of w, that is, ℓ(w sᵢ) + 1 = ℓ(w).

Tits' theorem, that ρ is injective, follows at once: an element w ≠ 1 has a right descent, so it makes a simple root negative and cannot act as the identity. Neither statement involves a finiteness hypothesis or the nondegeneracy of the canonical form: the proof inducts on a finite word and looks only at one two-generator standard parabolic subgroup at each step.

The file also records the elementary properties of the set of roots, the orbit of the simple roots: it is stable under W and under negation, its vectors are nonzero of norm one for the canonical form (which need not be positive definite), each of them is positive or negative, and a simple reflection permutes the positive roots other than its own simple root.

Main definitions

• CoxeterSystem.geometricRoots: the roots, the W-orbit of the simple roots.

Main results

• CoxeterSystem.geometricRepresentation_single_pos_iff and CoxeterSystem.geometricRepresentation_single_neg_iff: the geometric sign criterion.
• CoxeterSystem.geometricRepresentation_injective: Tits' theorem.
• CoxeterSystem.pos_or_neg_of_mem_geometricRoots: every root is positive or negative.
• CoxeterSystem.bijOn_geometricReflection_geometricRoots: a simple reflection permutes the positive roots other than its own simple root.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 5.4.

The sign criterion

theorem CoxeterSystem.exists_nonneg_geometricRepresentation_of_mem_parabolic_pair {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {i j : I} {v : W} (hv : v ∈ cs.parabolic {i, j}) (hvi : ¬cs.IsRightDescent v i) : ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ (cs.geometricRepresentation v) (Finsupp.single i 1) = a • Finsupp.single i 1 + b • Finsupp.single j 1

The rank-two case of the sign criterion. An element v of the standard parabolic subgroup on {i, j} without right descent at i sends the simple root αᵢ to a nonnegative combination of αᵢ and αⱼ.

theorem CoxeterSystem.geometricRepresentation_single_pos_iff {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (w : W) (i : I) : 0 < (cs.geometricRepresentation w) (Finsupp.single i 1) ↔ ¬cs.IsRightDescent w i

The geometric sign criterion, positive case. The root ρ(w) αᵢ is positive exactly when i is not a right descent of w, that is, when ℓ(w sᵢ) = ℓ(w) + 1.

theorem CoxeterSystem.geometricRepresentation_single_neg_iff {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (w : W) (i : I) : (cs.geometricRepresentation w) (Finsupp.single i 1) < 0 ↔ cs.IsRightDescent w i

The geometric sign criterion, negative case. The root ρ(w) αᵢ is negative exactly when i is a right descent of w, that is, when ℓ(w sᵢ) + 1 = ℓ(w).

theorem CoxeterSystem.geometricRepresentation_injective {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) : Function.Injective ⇑cs.geometricRepresentation

Tits' theorem: the standard geometric representation of a Coxeter system is faithful.

The roots

def CoxeterSystem.geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) : Set (I →₀ ℝ)

The roots of a Coxeter system: the vectors ρ(w) αᵢ of the W-orbit of the simple roots in the geometric representation. The orbit condition is essential, since a positive vector need not be a root: every root has norm one for the canonical form.

theorem CoxeterSystem.mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} : v ∈ cs.geometricRoots ↔ ∃ (w : W) (i : I), (cs.geometricRepresentation w) (Finsupp.single i 1) = v

@[simp]

theorem CoxeterSystem.single_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (i : I) : Finsupp.single i 1 ∈ cs.geometricRoots

The simple roots are roots.

@[simp]

theorem CoxeterSystem.geometricRepresentation_apply_mem_geometricRoots_iff {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (w : W) {v : I →₀ ℝ} : (cs.geometricRepresentation w) v ∈ cs.geometricRoots ↔ v ∈ cs.geometricRoots

The set of roots is stable under W.

theorem CoxeterSystem.geometricReflection_apply_mem_geometricRoots_iff {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (i : I) {v : I →₀ ℝ} : (M.geometricReflection i) v ∈ cs.geometricRoots ↔ v ∈ cs.geometricRoots

The set of roots is stable under each simple reflection.

@[simp]

theorem CoxeterSystem.neg_mem_geometricRoots_iff {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} : -v ∈ cs.geometricRoots ↔ v ∈ cs.geometricRoots

The set of roots is stable under negation.

theorem CoxeterSystem.geometricForm_self_of_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} (hv : v ∈ cs.geometricRoots) : (M.geometricForm v) v = 1

Roots have norm one for the canonical form, which need not be positive definite.

theorem CoxeterSystem.pos_or_neg_of_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} (hv : v ∈ cs.geometricRoots) : 0 < v ∨ v < 0

Every root is positive or negative.

theorem CoxeterSystem.ne_zero_of_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} (hv : v ∈ cs.geometricRoots) : v ≠ 0

Roots are nonzero.

theorem CoxeterSystem.eq_single_or_eq_neg_single_of_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} {i : I} (hv : v ∈ cs.geometricRoots) (hsupp : ∀ (j : I), j ≠ i → v j = 0) : v = Finsupp.single i 1 ∨ v = -Finsupp.single i 1

A root supported at the single index i is αᵢ or -αᵢ, because it has norm one.

theorem CoxeterSystem.geometricReflection_pos_of_mem_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) {v : I →₀ ℝ} {i : I} (hv : v ∈ cs.geometricRoots) (hpos : 0 < v) (hne : v ≠ Finsupp.single i 1) : 0 < (M.geometricReflection i) v

A simple reflection keeps every positive root other than its own simple root positive.

theorem CoxeterSystem.bijOn_geometricReflection_geometricRoots {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (i : I) : Set.BijOn ⇑(M.geometricReflection i) {v : I →₀ ℝ | v ∈ cs.geometricRoots ∧ 0 < v ∧ v ≠ Finsupp.single i 1} {v : I →₀ ℝ | v ∈ cs.geometricRoots ∧ 0 < v ∧ v ≠ Finsupp.single i 1}

A simple reflection permutes the positive roots other than its own simple root.