Each simple reflection $s_i$ in a Coxeter system is an involution, so $s_i^{-1} = s_i$.
A bundle of data realising a chamber complex $\mathcal{C}$ as the Coxeter complex of a Coxeter system $(W, S)$: chambers are indexed by $W$, the chamber map intertwines adjacency with right multiplication by simple reflections, the complex is thin, and the exchange condition together with a folding-from-half axiom holds.
- cc : ChamberComplex V
- B : Type u_3
- M : CoxeterMatrix self.B
- cs : CoxeterSystem self.M self.M.Group
- chamberOf_injective : Function.Injective self.chamberOf
- exchange : Garrett.ExchangeDeletion.SatisfiesExchangeCondition self.M self.cs
- folding_from_chamber_map (f₀ : self.M.Group → self.M.Group) : (∀ (w : self.M.Group), f₀ (f₀ w) = f₀ w) → (∀ (w : self.M.Group) (i : self.B), self.chamberOf (f₀ (w * self.cs.simple i)) = self.chamberOf (f₀ w) ∨ self.cc.Adjacent (self.chamberOf (f₀ w)) (self.chamberOf (f₀ (w * self.cs.simple i)))) → (∃ (w : self.M.Group), f₀ w ≠ w) → (∀ (w : self.M.Group), f₀ w = w → ∃! w' : self.M.Group, w' ≠ w ∧ f₀ w' = w) → ∃ (f : self.cc.Folding), ∀ (w : self.M.Group), Finset.image f.morph.toFun (self.chamberOf w) = self.chamberOf (f₀ w)
Instances For
The half-fold map $f_0^s : W \to W$ associated to a simple reflection $s$: elements $w$ with $\ell(sw) = \ell(w) + 1$ are fixed (the positive half), and elements with $\ell(sw) = \ell(w) - 1$ are sent to $sw$ (collapsing the negative half onto the positive half).
Instances For
$w$ lies in the positive half-space of the wall associated to $s$, i.e. $\ell(sw) = \ell(w) + 1$.
Instances For
$w$ lies in the negative half-space of the wall associated to $s$, i.e. $\ell(sw) + 1 = \ell(w)$.
Instances For
Every group element is on exactly one side of the wall: either in the positive or in the negative half.
The identity element lies in the positive half for every simple reflection $s$.
The simple reflection $s$ itself lies in the negative half for $s$.
$f_0^s$ fixes positive-half elements.
$f_0^s$ sends negative-half elements $w$ to $sw$.
Left multiplication by $s$ flips a positive-half element into the negative half.
Left multiplication by $s$ flips a negative-half element into the positive half.
The half-fold map $f_0^s$ is idempotent: $f_0^s \circ f_0^s = f_0^s$.
$f_0^s$ fixes the identity.
$f_0^s$ folds the simple reflection $s$ onto the identity.
Every fixed point $w$ of the half-fold map has a unique preimage outside itself, namely $sw$ — the map is exactly two-to-one onto the positive half.
A length-descending step $w \mapsto ws_t$ cannot simultaneously cross from the positive half to the negative half.
A length-ascending step $w \mapsto ws_t$ cannot simultaneously cross from the negative half to the positive half.
Adjacent chambers $C_w$ and $C_{ws_t}$ are sent by the chamber map of $f_0^s$ to chambers that are either equal or still adjacent — folds do not tear adjacencies apart.
Left multiplication by $w$ on $W$ preserves chamber adjacency: if $C_a$ and $C_b$ are adjacent, so are $C_{wa}$ and $C_{wb}$.
The conjugate $u \mapsto w \cdot f_0^s(w^{-1}u)$ of the half-fold map by left translation by $w$ — gives the folding that pairs the chambers $C_w$ and $C_{ws}$.
Instances For
The conjugated fold fixes the base chamber $C_w$.
The conjugated fold sends the neighbour $C_{ws}$ across the wall back to $C_w$.
The conjugated fold is idempotent.
The conjugated fold is not the identity: it moves at least one element.
Each fixed point of the conjugated fold has a unique preimage outside itself, namely $wsw^{-1}u$.
The chamber map of the conjugated fold preserves adjacency: adjacent chambers $C_u, C_{us_t}$ go to chambers that are equal or still adjacent.