noncomputable def ChamberComplex.coxeterHalfGroupMap {B_idx : Type u_2} (M : CoxeterMatrix B_idx) (i : B_idx) (w : M.Group) : M.Group

The group-level half-apartment map for simple reflection $s_i$: returns $w$ if multiplication by $s_i$ on the left lengthens $w$, and $s_i w$ otherwise.

theorem ChamberComplex.coxeterHalfGroupMap_idempotent {B_idx : Type u_2} (M : CoxeterMatrix B_idx) (i : B_idx) (w : M.Group) : coxeterHalfGroupMap M i (coxeterHalfGroupMap M i w) = coxeterHalfGroupMap M i w

The half-apartment map $\text{coxeterHalfGroupMap}_i$ is idempotent on the Coxeter group.

noncomputable def ChamberComplex.coxeterHalfChamberMap {V : Type u_1} [DecidableEq V] {B_idx : Type u_2} (K : ChamberComplex V) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (i : B_idx) (E : Finset V) : Finset V

Lift coxeterHalfGroupMap from the Coxeter group to the chamber complex along a labelling $\varphi$: maps chamber $E$ to a chamber whose $\varphi$-image equals the half-apartment image of $\varphi(E)$.

theorem ChamberComplex.coxeterHalfChamberMap_spec {V : Type u_1} [DecidableEq V] {B_idx : Type u_2} (K : ChamberComplex V) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (i : B_idx) (E : Finset V) : φ (K.coxeterHalfChamberMap M φ hsurj i E) = coxeterHalfGroupMap M i (φ E)

The chamber-level half map intertwines with the group-level map along $\varphi$: $\varphi(\text{coxeterHalfChamberMap}\ i\ E) = \text{coxeterHalfGroupMap}\ i\ (\varphi(E))$.

theorem ChamberComplex.coxeterHalfChamberMap_maximal {V : Type u_1} [DecidableEq V] {B_idx : Type u_2} (K : ChamberComplex V) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (i : B_idx) (E : Finset V) (hE : K.IsMaximal E) : K.IsMaximal (K.coxeterHalfChamberMap M φ hsurj i E)

The chamber-level half map preserves maximality (chambers go to chambers).