theorem thin_unique_other_chamber {V : Type} [DecidableEq V] (cc : ChamberComplex V) (hthin : cc.IsThin) (F C : Finset V) (hFC : cc.IsFacet F C) (hC : cc.IsMaximal C) : ∃! D : Finset V, D ≠ C ∧ cc.IsFacet F D ∧ cc.IsMaximal D

In a thin chamber complex, each facet $F$ of a chamber $C$ lies in exactly one other chamber $D \ne C$.

theorem coxeter_lab_card_eq_face_card {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (s : Finset V) (hs : s ∈ A.faces) : (lab s).card = s.card

In a Coxeter complex, a strictly monotone labelling on faces has $|\text{lab}(s)| = |s|$ for every face $s$.

theorem coxeter_lab_vertex_in_face_label {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (s : Finset V) (hs : s ∈ A.faces) (ℓ : L) (hℓ : ℓ ∈ lab s) : ∃ v ∈ s, ℓ ∈ lab {v}

Each label in $\text{lab}(s)$ already appears in the label of some vertex $v \in s$.

theorem coxeter_lab_surj_on_chamber {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (C : Finset V) (hC : A.IsMaximal C) (ℓ : L) : ℓ ∈ lab C

On a chamber $C$, the labelling $\text{lab}$ is surjective onto $\text{lab}(C)$.

theorem coxeter_single_labelling_factors {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (C : Finset V) (hC : A.IsMaximal C) : ∃ (τ : V → L), (∀ s ∈ A.faces, lab s = Finset.image τ s) ∧ Set.InjOn τ ↑C ∧ ∀ (ℓ : L), ∃ v ∈ C, τ v = ℓ

A labelling of a Coxeter complex factors through a vertex-level map: $\text{lab}(s) = \{\sigma(v) \mid v \in s\}$ for some $\sigma : V \to L$.

theorem coxeter_vertex_type_pointwise_compat {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (C : Finset V) (hC : A.IsMaximal C) (hagree : lab₂ C = Finset.image f (lab₁ C)) (τ₁ : V → L₁) (hτ₁ : ∀ s ∈ A.faces, lab₁ s = Finset.image τ₁ s) (τ₂ : V → L₂) (hτ₂ : ∀ s ∈ A.faces, lab₂ s = Finset.image τ₂ s) (v : V) (hv : v ∈ C) : τ₂ v = f (τ₁ v)

The vertex-level labelling is pointwise compatible: the label of a vertex matches the singleton label of that vertex.

theorem coxeter_subface_label_compat {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (C : Finset V) (hC : A.IsMaximal C) (hagree : lab₂ C = Finset.image f (lab₁ C)) (s : Finset V) (hs : s ∈ A.faces) (hsC : s ⊆ C) : lab₂ s = Finset.image f (lab₁ s)

A labelling on a face is compatible with subface labels: removing a vertex removes its label from the labelling.

theorem coxeter_vertex_type_function {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (C : Finset V) (hC : A.IsMaximal C) (hagree : lab₂ C = Finset.image f (lab₁ C)) : ∃ (τ₁ : V → L₁) (τ₂ : V → L₂), (∀ s ∈ A.faces, lab₁ s = Finset.image τ₁ s) ∧ (∀ s ∈ A.faces, lab₂ s = Finset.image τ₂ s) ∧ (∀ v ∈ C, τ₂ v = f (τ₁ v)) ∧ Set.InjOn τ₁ ↑C ∧ ∀ (ℓ : L₁), ∃ v ∈ C, τ₁ v = ℓ

The vertex-type function $\sigma : V \to L$ associated to a Coxeter labelling, extracted from the chamber-level labels.

theorem coxeter_chamber_labels_surj {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (C₀ : Finset V) (hC₀ : A.IsMaximal C₀) : (∀ (ℓ : L), ℓ ∈ lab C₀) ∧ (lab C₀).card = C₀.card

The labelling is surjective on each chamber: every label appears on some vertex of the chamber.

theorem coxeter_chambers_same_label_set {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L : Type) [DecidableEq L] (lab : Finset V → Finset L) (hmono : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab s ⊂ lab t) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : lab C = lab D

Any two chambers of a Coxeter complex have the same label set.

theorem coxeter_adj_label_step {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (C₁ C₂ : Finset V) (hadj : A.Adjacent C₁ C₂) (hagree : lab₂ C₁ = Finset.image f (lab₁ C₁)) : lab₂ C₂ = Finset.image f (lab₁ C₂)

Adjacent chambers differ in label by exactly one vertex.

theorem coxeter_subface_label_step {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (C : Finset V) (hC : A.IsMaximal C) (hagree : lab₂ C = Finset.image f (lab₁ C)) (s : Finset V) (hs : s ∈ A.faces) (hsC : s ⊆ C) : lab₂ s = Finset.image f (lab₁ s)

A subface labelling step: how the labels of $s \cup \{v\}$ relate to those of $s$.

theorem coxeter_label_bijection_exists {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (C₀ : Finset V) (hC₀ : A.IsMaximal C₀) : ∃ (f : L₁ → L₂), Function.Bijective f ∧ lab₂ C₀ = Finset.image f (lab₁ C₀)

Existence of a label bijection between any two chambers compatible with the vertex labelling.

theorem coxeter_label_agree_along_chain {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj_φ : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hmono₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hmono₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (f : L₁ → L₂) (hf : Function.Bijective f) (cs : List (Finset V)) (hne : cs ≠ []) (hchain : List.IsChain A.Adjacent cs) (hall : ∀ C ∈ cs, A.IsMaximal C) (hagree_head : lab₂ (cs.head hne) = Finset.image f (lab₁ (cs.head hne))) (D : Finset V) : D ∈ cs → lab₂ D = Finset.image f (lab₁ D)

The Coxeter labelling is determined along a gallery: agreement at one chamber forces agreement throughout the chain.

theorem coxeter_complex_unique_labelling_axiom {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) : (∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) → (∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) → ∀ (C₀ : Finset V), A.IsMaximal C₀ → (∃ (f : L₁ → L₂), Function.Bijective f ∧ lab₂ C₀ = Finset.image f (lab₁ C₀)) ∧ ∀ (f : L₁ → L₂), Function.Bijective f → lab₂ C₀ = Finset.image f (lab₁ C₀) → ∀ s ∈ A.faces, lab₂ s = Finset.image f (lab₁ s)

The Coxeter complex satisfies the unique-labelling property: any two labellings agreeing on a single chamber agree everywhere.