theorem ChamberComplex.finset_image_eq_of_agree {V : Type u_1} [DecidableEq V] {s E : Finset V} {r f : V → V} (hsE : s ⊆ E) (heq : ∀ v ∈ E, r v = f v) : Finset.image r s = Finset.image f s

Two functions $r, f$ agreeing on a superset $E \supseteq s$ produce the same image on $s$.

theorem ChamberComplex.wallReflection_eq_g_on_fixed {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (wr : X.WallReflection) {E : Finset V} (hfE : Finset.image wr.rf.f.morph.toFun E = E) (v : V) : v ∈ E → wr.refl v = wr.rf.g.morph.toFun v

On a face fixed by the folding $f$, the wall reflection $s$ agrees with the opposite folding $g$.

theorem ChamberComplex.wallReflection_eq_f_on_moved {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (wr : X.WallReflection) {E : Finset V} (hEmax : X.IsMaximal E) (hfE : Finset.image wr.rf.f.morph.toFun E ≠ E) (v : V) : v ∈ E → wr.refl v = wr.rf.f.morph.toFun v

On a face moved by the folding $f$, the wall reflection agrees with $f$.

theorem ChamberComplex.wallReflection_maps_faces {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (wr : X.WallReflection) (s : Finset V) (hs : s ∈ X.faces) : Finset.image wr.refl s ∈ X.faces

A wall reflection acts on faces of the chamber complex, sending faces to faces.

theorem ChamberComplex.list_comp_bijective {V : Type u_1} [DecidableEq V] (fs : List (V → V)) : (∀ f ∈ fs, Function.Bijective f) → Function.Bijective (List.foldr (fun (x1 x2 : V → V) => x1 ∘ x2) id fs)

The composition of a list of bijective functions is bijective.

theorem ChamberComplex.wallReflection_maps_chamber {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (wr : X.WallReflection) {C D : Finset V} (hDmax : X.IsMaximal D) (hfC : Finset.image wr.rf.f.morph.toFun C = C) (hfD : Finset.image wr.rf.f.morph.toFun D = C) (hne : C ≠ D) : Finset.image wr.refl D = C

The wall reflection sends the chamber $D$ across the panel to the opposite chamber $C$.

theorem ChamberComplex.chain_compose {V : Type u_1} [DecidableEq V] {faces : Set (Finset V)} {R : Finset V → Finset V → Prop} (l : List (Finset V)) (hchain : List.IsChain R l) (hmaps : ∀ (x y : Finset V), R x y → ∃ (φ : V → V), Function.Bijective φ ∧ (∀ s ∈ faces, Finset.image φ s ∈ faces) ∧ (∀ (s : Finset V), Finset.image φ s ∈ faces → s ∈ faces) ∧ Finset.image φ x = y) (hne : l ≠ []) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ s ∈ faces, Finset.image φ s ∈ faces) ∧ (∀ (s : Finset V), Finset.image φ s ∈ faces → s ∈ faces) ∧ Finset.image φ (l.head hne) = l.getLast hne

Compose a sequence of vertex maps witnessing the steps of a gallery chain into a single composed map.

theorem ChamberComplex.apt_vertex_level_automorphism {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (hWR : ∀ (C D : Finset V), A.Adjacent C D → ∃ (wr : cc.WallReflection), Finset.image wr.refl D = C) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A.faces) ∧ Finset.image φ D = C

Vertex-level automorphism of an apartment: a bijective vertex map realising chamber transitivity.

theorem coxeter_3clause_hasSufficientReversibleFoldings {V : Type} [DecidableEq V] (cc : ChamberComplex V) (hThin : cc.IsThin) (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), cc.IsMaximal C → ∀ (D : Finset V), cc.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), cc.IsMaximal C ∧ φ C = w) (hadj_fwd : ∀ (C C' : Finset V), cc.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) : cc.HasSufficientReversibleFoldings

A Coxeter complex has sufficient reversible foldings: every adjacent pair of chambers is collapsed by a reversible folding.

noncomputable def reversibleFolding_to_wallReflection {V : Type} [DecidableEq V] (cc : ChamberComplex V) (rf : cc.ReversibleFolding) : cc.WallReflection

Convert a reversible folding to the associated wall reflection.

theorem reversibleFolding_to_wallReflection_rf {V : Type} [DecidableEq V] (cc : ChamberComplex V) (rf : cc.ReversibleFolding) : (reversibleFolding_to_wallReflection cc rf).rf = rf

The conversion reversibleFolding_to_wallReflection recovers the underlying reversible folding.

theorem coxeter_apt_wall_reflections {V : Type} [DecidableEq V] (cc : ChamberComplex V) (A : SimplicialComplex V) (hcc : cc.toSimplicialComplex = A) (hThin : cc.IsThin) (hCox : ∃ (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) ∧ (∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) ∧ ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (C D : Finset V) : A.Adjacent C D → ∃ (wr : cc.WallReflection), Finset.image wr.refl D = C

A Coxeter apartment has enough wall reflections: every pair of adjacent chambers is exchanged by some wall reflection.