theorem coxeter_link_gallery_connected {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) (C D : Finset V) : (A.linkComplex σ hσ).IsMaximal C → (A.linkComplex σ hσ).IsMaximal D → ∃ (g : Gallery (A.linkComplex σ hσ)), g.chambers.head? = some C ∧ g.chambers.getLast? = some D

Gallery-connectedness of the link of a face $\sigma$ in a Coxeter complex $A$: any two chambers of $\mathrm{lk}_A(\sigma)$ are joined by a gallery, using the Coxeter labelling of $A$ via its parabolic subgroup structure.

theorem coxeter_labeling_implies_thin {V : Type u_1} [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')) : cc.IsThin

A chamber complex equipped with a Coxeter labelling (injective, surjective, and adjacency-preserving) is thin: each codimension-one face is contained in exactly two chambers.

theorem link_thin_of_ambient_thin {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (hcc_thin : cc.IsThin) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) (cc' : ChamberComplex V) (hcc'_eq : cc'.toSimplicialComplex = A.linkComplex σ hσ) : cc'.IsThin

Thinness is inherited by links: if $A$ has a thin chamber complex structure $cc$, then the link $\mathrm{lk}_A(\sigma)$ is also thin under any chamber complex structure $cc'$.

theorem coxeter_link_thin {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) (cc' : ChamberComplex V) (hcc'_eq : cc'.toSimplicialComplex = A.linkComplex σ hσ) : cc'.IsThin

The link of a face in a Coxeter complex is thin, combining coxeter_labeling_implies_thin and link_thin_of_ambient_thin.

theorem linkComplex_maximal_of_union_maximal_local {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {σ : Finset V} (hσ : σ ∈ K.faces) {τ : Finset V} (hτ_link : τ ∈ (K.linkComplex σ hσ).faces) (hστ_max : K.IsMaximal (σ ∪ τ)) : (K.linkComplex σ hσ).IsMaximal τ

Local version of linkComplex_maximal_of_union_maximal: if $\sigma \cup \tau$ is a maximal face of $K$ and $\tau$ lies in $\mathrm{lk}_K(\sigma)$, then $\tau$ is maximal in the link.

theorem link_cc_exists_maximal {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) (s : Finset V) : s ∈ (A.linkComplex σ hσ).faces → ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ s ⊆ C

Existence-of-maximal-faces axiom for the chamber complex structure on a link: every face of $\mathrm{lk}_A(\sigma)$ extends to a maximal face.

theorem link_has_chamber_complex_structure {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (cc' : ChamberComplex V), cc'.toSimplicialComplex = A.linkComplex σ hσ ∧ cc'.IsThin

The link of a face in a Coxeter complex carries a thin chamber complex structure, packaging the existence of maximals, gallery-connectedness, and thinness.

theorem link_coxeter_labeling_from_restricted {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (T : Set B_idx) (φ' : Finset V → (M.restrictToSet T).Group), (∀ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C → ∀ (D : Finset V), (A.linkComplex σ hσ).IsMaximal D → φ' C = φ' D → C = D) ∧ (∀ (w : (M.restrictToSet T).Group), ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ φ' C = w) ∧ ∀ (C C' : Finset V), (A.linkComplex σ hσ).Adjacent C C' → CoxeterComplex.ChamberAdjacent (M.restrictToSet T) (φ' C) (φ' C')

Restricted Coxeter labelling for the link: there exists a subset $T \subseteq B_{\mathrm{idx}}$ of generators and a Coxeter labelling of $\mathrm{lk}_A(\sigma)$ valued in the parabolic subgroup $\langle T \rangle$.

theorem parabolic_coset_labeling_full {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (B_idx' : Type) (M' : CoxeterMatrix B_idx') (φ' : Finset V → M'.Group), (∀ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C → ∀ (D : Finset V), (A.linkComplex σ hσ).IsMaximal D → φ' C = φ' D → C = D) ∧ (∀ (w : M'.Group), ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ φ' C = w) ∧ ∀ (C C' : Finset V), (A.linkComplex σ hσ).Adjacent C C' → CoxeterComplex.ChamberAdjacent M' (φ' C) (φ' C')

Repackaging the restricted Coxeter labelling as a full Coxeter labelling on the parabolic subgroup $M' := M|_T$, giving a Coxeter labelling of $\mathrm{lk}_A(\sigma)$.

theorem link_has_coxeter_labeling {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (B_idx' : Type) (M' : CoxeterMatrix B_idx') (φ' : Finset V → M'.Group), (∀ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C → ∀ (D : Finset V), (A.linkComplex σ hσ).IsMaximal D → φ' C = φ' D → C = D) ∧ (∀ (w : M'.Group), ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ φ' C = w) ∧ ∀ (C C' : Finset V), (A.linkComplex σ hσ).Adjacent C C' → CoxeterComplex.ChamberAdjacent M' (φ' C) (φ' C')

The link $\mathrm{lk}_A(\sigma)$ of a face $\sigma$ in a Coxeter complex carries a Coxeter labelling, expressed via parabolic_coset_labeling_full.

theorem coxeter_link_is_sub_coxeter {V : Type u_1} [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')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (B_idx' : Type) (M' : CoxeterMatrix B_idx') (cc' : ChamberComplex V), cc'.toSimplicialComplex = A.linkComplex σ hσ ∧ ∃ (φ' : Finset V → M'.Group), (∀ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C → ∀ (D : Finset V), (A.linkComplex σ hσ).IsMaximal D → φ' C = φ' D → C = D) ∧ (∀ (w : M'.Group), ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ φ' C = w) ∧ (∀ (C C' : Finset V), (A.linkComplex σ hσ).Adjacent C C' → CoxeterComplex.ChamberAdjacent M' (φ' C) (φ' C')) ∧ cc'.IsThin

The link of a face in a Coxeter complex is again a (sub-)Coxeter complex: it carries a thin chamber complex structure together with a Coxeter labelling, combining link_has_chamber_complex_structure and link_has_coxeter_labeling.