LemmaStatement: Literature-sourcedProof: AI-generated

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.

Finite root difference forces finite connected parabolic

PDF p. 11: Lemma 3.20(1)

Statement

For $I \subseteq Γ_{0}$ and $a \in I^{c}$ , if $∣ Φ_{I + a} ∖ Φ_{I} ∣ < \infty$ , then $W_{[I, a]}$ is finite.

Statement references

Coxeter-system, roots, length and weak-order conventions

Connected component notation [I,a]

Standard parabolic subgroups and parabolic roots

Facts & Assumptions

[F1]

Finite $D$ implies that $K$ and $W_{J}$ are finite by Finite outside roots give a finite complementary parabolic.

[F2]

For finite $L$ , $W_{L}$ is finite if and only if $Φ_{L}$ is finite by Finite roots and finite Coxeter groups at finite rank.

[F3]

One has $Φ_{K} \cap Φ_{I} = Φ_{J}$ and $Φ_{K} ∖ Φ_{J} \subseteq D$ by Component roots intersect the complementary parabolic exactly.

Proof

Given: fix the possibly infinite-rank Coxeter system $(W, S)$ , its associated diagram $Γ$ on $Γ_{0}$ , and its standard geometric root representation as in Coxeter-system, roots, length and weak-order conventions. Take the parabolic root sets of Standard parabolic subgroups and parabolic roots for this same system and $K = [I, a]$ as in Connected component notation [I,a] for this diagram. Put $J = K ∖ {a}$ and $D = Φ_{I + a} ∖ Φ_{I}$ , and assume $D$ is finite. Goal: prove $W_{K}$ finite, without a finite ambient-rank assumption.

Proof technique: direct.

1.1F1F2given

By [F1], $K$ is finite and $W_{J}$ is finite. Since $J \subseteq K$ is finite, [F2] gives that $Φ_{J}$ is finite.

2.1F2F3step 1.1given∎

By [F3], every element of $Φ_{K}$ lies either in $Φ_{J}$ or in the finite set $D$ . Thus $Φ_{K} \subseteq Φ_{J} \cup D$ is finite. Since $K$ is finite, [F2] now gives $W_{K} = W_{[I, a]}$ finite, as required.

Source notes

The frozen article attributes this claim to [24, Lemma 1.40]. The accessible independent Iyama–Wemyss author manuscript (PDF metadata dated 23 June 2020; https://www.maths.gla.ac.uk/~mwemyss/MainFile_for_web.pdf) has different numbering and does not contain that locator. Its §§1.1–1.3 (printed pp. 3–4; PDF pp. 27–28) were inspected for presentation, parabolic and reflection conventions only; no matching theorem or proof was verified there. The proof above instead uses finite invariant root sets and propagation along connected diagram paths. It is an independent local derivation, not a reconstruction of the unread cited Lemma 1.40.

Depends on

Used by · 1

Adjacent relative chambers force a finite crossing component

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Normalisers of parabolic subgroups of Artin–Tits groups and Tits cone intersections · PDF pp. 11; Lemma 3.20(1)