structure ChamberComplex.CoxeterProperties {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

The combinatorial Coxeter properties of a chamber complex: thinness plus, for every adjacent pair $C \sim D$, a folding that fixes $C$ and sends $D$ to $C$.

• thin : K.IsThin
• folding_maps_adj_to_self (C D : Finset V) : K.Adjacent C D → ∃ (f : K.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun D = C

def ChamberComplex.SeparatedByWall {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (C D : Finset V) : Prop

Two chambers $C, D$ are separated by a wall if some reversible folding places them on opposite sides.

def ChamberComplex.IsCoxeterComplex {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

$K$ is a Coxeter complex: it carries a bijective labelling $\varphi : \text{chambers} \to W$ into a Coxeter group $W$ such that adjacency corresponds to right multiplication by a simple generator, every facet is shared by at least one other chamber.

def ChamberComplex.HasSufficientReversibleFoldings {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

$K$ has sufficient reversible foldings: every adjacent pair admits a reversible folding swapping them as boundary chambers of the wall.

theorem ChamberComplex.hasSufficientReversibleFoldings_folding_maps_adj_to_self {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hSRF : K.HasSufficientReversibleFoldings) (C D : Finset V) : K.Adjacent C D → ∃ (f : K.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun D = C

Sufficient reversible foldings give the "folding maps adjacent to self" condition.

def ChamberComplex.coxeterProperties_of_hasSufficientReversibleFoldings {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hThin : K.IsThin) (hSRF : K.HasSufficientReversibleFoldings) : K.CoxeterProperties

Assemble CoxeterProperties K from thinness plus sufficient reversible foldings.

theorem ChamberComplex.hasSufficientReversibleFoldings_separatedByWall {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hSRF : K.HasSufficientReversibleFoldings) (C D : Finset V) (hadj : K.Adjacent C D) : K.SeparatedByWall C D

Sufficient reversible foldings imply that every adjacent pair is separated by a wall.

theorem ChamberComplex.separatedByWall_hasSufficientReversibleFoldings {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hThin : K.IsThin) (hSep : ∀ (C D : Finset V), K.Adjacent C D → K.SeparatedByWall C D) : K.HasSufficientReversibleFoldings

Converse: in a thin complex, "adjacent chambers separated by a wall" implies sufficient reversible foldings.

theorem ChamberComplex.hasSufficientReversibleFoldings_hasSufficientFoldings {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hSRF : K.HasSufficientReversibleFoldings) : AptIsCoxeterProof.HasSufficientFoldings K

Sufficient reversible foldings imply the (one-sided) "sufficient foldings" condition used in the Tits/AptIsCoxeter proof.

theorem ChamberComplex.isCoxeterComplex_thinWithFoldings {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) : K.IsCoxeterComplex → K.IsThin ∧ K.HasSufficientReversibleFoldings

One direction of the characterization: every Coxeter complex is thin and has sufficient reversible foldings.

theorem ChamberComplex.thinWithFoldings_isCoxeterComplex {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) : K.IsThin → AptIsCoxeterProof.HasSufficientFoldings K → K.IsCoxeterComplex

Converse of the characterization: a thin chamber complex with sufficient foldings is a Coxeter complex.

theorem ChamberComplex.coxeter_iff_adjacent_separated_by_wall {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : K.IsCoxeterComplex ↔ K.IsThin ∧ ∀ (C D : Finset V), K.Adjacent C D → K.SeparatedByWall C D

Main characterization: $K$ is a Coxeter complex iff $K$ is thin and every adjacent pair of chambers is separated by a wall.

theorem ChamberComplex.injective_image_ne_of_ne {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (f : K.Morphism K.toSimplicialComplex) (hinj : Function.Injective f.toFun) {C D : Finset V} (_hC : C ∈ K.faces) (_hD : D ∈ K.faces) (hne : C ≠ D) : Finset.image f.toFun C ≠ Finset.image f.toFun D

An injective vertex map sends distinct chambers to distinct image chambers.

theorem ChamberComplex.injective_no_stutter {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (f : K.Morphism K.toSimplicialComplex) (hinj : Function.Injective f.toFun) (γ : Gallery K.toSimplicialComplex) : ¬ImageGalleryStutters f γ.chambers

The image of a gallery under an injective map never stutters.