def SimplicialComplex.HasFiniteDiameter {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (d : ℕ) : Prop

A simplicial complex has finite diameter bounded by $d$ if every pair of chambers has gallery distance at most $d$.

def Building.HasFiniteDiameter {V : Type u_1} [DecidableEq V] (b : Building V) (d : ℕ) : Prop

A building has finite diameter if its underlying chamber complex does.

theorem chain_word_bound {W : Type u_2} [Group W] {B : Type u_3} {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List W) (hne : l ≠ []) (h_chain : List.IsChain (fun (w w' : W) => ∃ (i : B), w' = w * cs.simple i) l) : cs.length ((l.head hne)⁻¹ * l.getLast hne) ≤ l.length - 1

A length bound for words in a Coxeter group: the length of any representation of $w$ is bounded by the diameter.

theorem ischain_map {α : Type u_2} {β : Type u_3} {R : α → α → Prop} {S : β → β → Prop} {f : α → β} (hRS : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (h : List.IsChain R l) : List.IsChain S (List.map f l)

Pushforward of a chain under a relation-respecting map.

theorem word_length_le_galleryDist {V : Type u_2} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (_hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (C D : Finset V) : A.IsMaximal C → A.IsMaximal D → M.toCoxeterSystem.length ((φ C)⁻¹ * φ D) ≤ galleryDist A C D

The Coxeter length of any word is at most the gallery distance between the corresponding chambers.

theorem coxeter_complex_finite_diameter_implies_finite {V : Type u_2} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) [Fintype B_idx] (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (d : ℕ) (hd : A.HasFiniteDiameter d) (φ : Finset V → M.Group) (hφ_inj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hφ_surj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) : A.faces.Finite

A Coxeter complex of finite diameter is finite (has finitely many chambers).

theorem folding_has_reversible_pair {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (f : cc.Folding) : ∃ (rf : cc.ReversibleFolding), rf.f = f

Every folding in a Coxeter complex has a reversible pair: an opposite folding that complements it.

theorem coxeter_complex_foldings_reversible {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (f : cc.Folding) : ∃ (f' : cc.Folding), (∀ (D : Finset V), cc.IsMaximal D → (Finset.image f.morph.toFun D = D ↔ Finset.image f'.morph.toFun D ≠ D)) ∧ ∀ (D : Finset V), cc.IsMaximal D → Finset.image f.morph.toFun D = D → Finset.image f.morph.toFun (Finset.image f'.morph.toFun D) = D

Every folding in a Coxeter complex is reversible: it admits a paired opposite folding sending the fixed side to the moved side and vice versa.

theorem ApartmentSystem.apt_reversible_foldings_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding), ∃ (f' : cc.Folding), (∀ (D : Finset V), cc.IsMaximal D → (Finset.image f.morph.toFun D = D ↔ Finset.image f'.morph.toFun D ≠ D)) ∧ ∀ (D : Finset V), cc.IsMaximal D → Finset.image f.morph.toFun D = D → Finset.image f.morph.toFun (Finset.image f'.morph.toFun D) = D

In an apartment system, every folding of an apartment is reversible.

theorem adjacent_in_subcomplex' {V : Type u_2} [DecidableEq V] {A K : SimplicialComplex V} (_hsub : IsSubcomplex A K) {C D : Finset V} (hadj : K.Adjacent C D) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : A.Adjacent C D

Adjacency in a chamber subcomplex transfers to adjacency in the ambient complex.

theorem chain_transfer_to_subcomplex' {V : Type u_2} [DecidableEq V] {A K : SimplicialComplex V} (hsub : IsSubcomplex A K) (l : List (Finset V)) (hchain : List.IsChain K.Adjacent l) (hmax : ∀ E ∈ l, A.IsMaximal E) : List.IsChain A.Adjacent l

A gallery in a subcomplex remains a gallery in the ambient complex.

theorem adjacent_lift_to_supercomplex {V : Type u_2} [DecidableEq V] {A K : SimplicialComplex V} (hsub : IsSubcomplex A K) {C D : Finset V} (hadj : A.Adjacent C D) (hC_K : K.IsMaximal C) (hD_K : K.IsMaximal D) : K.Adjacent C D

Adjacency in a complex lifts to adjacency in a supercomplex containing both chambers.

theorem chain_lift_to_supercomplex {V : Type u_2} [DecidableEq V] {A K : SimplicialComplex V} (hsub : IsSubcomplex A K) (l : List (Finset V)) (hchain : List.IsChain A.Adjacent l) (hmax_K : ∀ E ∈ l, K.IsMaximal E) : List.IsChain K.Adjacent l

A chain (gallery) in a complex lifts to the same chain in a supercomplex.

theorem ApartmentSystem.apt_dist_eq_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (C D : Finset V), C ∈ A.faces → D ∈ A.faces → A.IsMaximal C → A.IsMaximal D → galleryDist A C D = galleryDist K.toSimplicialComplex C D

The gallery distance between chambers of an apartment $A$ equals the gallery distance computed in the ambient building.

theorem ApartmentSystem.fold_decreases_dist_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (C D : Finset V), cc.IsMaximal C → cc.IsMaximal D → Finset.image f.morph.toFun C = C → Finset.image f.morph.toFun D ≠ D → galleryDist cc.toSimplicialComplex C (Finset.image f.morph.toFun D) < galleryDist cc.toSimplicialComplex C D

A folding fixing $C$ strictly decreases distance to a moved chamber $D$.

theorem ApartmentSystem.fold_preserves_maximal_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (D : Finset V), cc.IsMaximal D → cc.IsMaximal (Finset.image f.morph.toFun D)

A folding sends maximal chambers to maximal chambers.

theorem galleryDist_eq_card_separating_foldings {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (A B : Finset V) (hAm : cc.IsMaximal A) (hBm : cc.IsMaximal B) : galleryDist cc.toSimplicialComplex A B = Nat.card { f : cc.Folding // ChamberComplex.OppositeSides f A B }

The gallery distance between two chambers equals the number of foldings that separate them.

theorem finite_separating_foldings {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (A B : Finset V) (hAm : cc.IsMaximal A) (hBm : cc.IsMaximal B) : Finite { f : cc.Folding // ChamberComplex.OppositeSides f A B }

For any pair of chambers in a spherical apartment, only finitely many foldings separate them.

theorem galleryDist_ge_of_walls_partition {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (C C' D : Finset V) (hCm : cc.IsMaximal C) (hDm : cc.IsMaximal D) (hC'm : cc.IsMaximal C') (Hopp : ∀ (f : cc.Folding), ChamberComplex.OppositeSides f C D) (Hpartition : ∀ (f : cc.Folding), ChamberComplex.OppositeSides f C C' ∨ ChamberComplex.OppositeSides f C' D) : galleryDist cc.toSimplicialComplex C C' + galleryDist cc.toSimplicialComplex C' D ≤ galleryDist cc.toSimplicialComplex C D

If the walls separating $C$ from $D$ partition into those separating $C$ from $C'$ and those separating $C'$ from $D$, the distance is at least the sum.

theorem gallery_concat_minimal_when_walls_partition {V : Type u_2} [DecidableEq V] (cc : ChamberComplex V) (C C' D : Finset V) (hCm : cc.IsMaximal C) (hDm : cc.IsMaximal D) (hC'm : cc.IsMaximal C') (Hopp : ∀ (f : cc.Folding), ChamberComplex.OppositeSides f C D) (Hpartition : ∀ (f : cc.Folding), ChamberComplex.OppositeSides f C C' ∨ ChamberComplex.OppositeSides f C' D) : galleryDist cc.toSimplicialComplex C D = galleryDist cc.toSimplicialComplex C C' + galleryDist cc.toSimplicialComplex C' D

Concatenating minimal galleries $C \to C'$ and $C' \to D$ is minimal when the separating walls partition.

theorem ApartmentSystem.wall_sep_additive_dist_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (C D C' : Finset V), cc.IsMaximal C → cc.IsMaximal D → cc.IsMaximal C' → (∀ (f : cc.Folding), ChamberComplex.OppositeSides f C D) → galleryDist cc.toSimplicialComplex C D = galleryDist cc.toSimplicialComplex C C' + galleryDist cc.toSimplicialComplex C' D

Additivity of distance across a wall-separating chamber: $d(C, D) = d(C, C') + d(C', D)$ when all foldings separate $C$ from $D$.

theorem ApartmentSystem.gallery_through_chamber_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (_𝒜 : ApartmentSystem K) (C C' D : Finset V) : K.IsMaximal C → K.IsMaximal C' → K.IsMaximal D → galleryDist K.toSimplicialComplex C D = galleryDist K.toSimplicialComplex C C' + galleryDist K.toSimplicialComplex C' D → ∃ (g : Gallery K.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist K.toSimplicialComplex C D ∧ C' ∈ g.chambers

When the additive distance condition holds, a minimal gallery from $C$ to $D$ can be chosen to pass through $C'$.

structure OppositeChamberHypGen {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) (𝒜 : ApartmentSystem K) : Prop

Bundle of hypotheses needed for the opposite-chamber theorem in the generic apartment-system setting: reversibility, distance equality, fold decreases distance, maximality preservation, additivity, and existence of galleries through chambers.

• apt_reversible_foldings (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding), ∃ (f' : cc.Folding), (∀ (D : Finset V), cc.IsMaximal D → (Finset.image f.morph.toFun D = D ↔ Finset.image f'.morph.toFun D ≠ D)) ∧ ∀ (D : Finset V), cc.IsMaximal D → Finset.image f.morph.toFun D = D → Finset.image f.morph.toFun (Finset.image f'.morph.toFun D) = D
• apt_dist_eq (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (C D : Finset V), C ∈ A.faces → D ∈ A.faces → A.IsMaximal C → A.IsMaximal D → galleryDist A C D = galleryDist K.toSimplicialComplex C D
• fold_decreases_dist (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (C D : Finset V), cc.IsMaximal C → cc.IsMaximal D → Finset.image f.morph.toFun C = C → Finset.image f.morph.toFun D ≠ D → galleryDist cc.toSimplicialComplex C (Finset.image f.morph.toFun D) < galleryDist cc.toSimplicialComplex C D
• fold_preserves_maximal (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (D : Finset V), cc.IsMaximal D → cc.IsMaximal (Finset.image f.morph.toFun D)
• wall_sep_additive_dist (A : SimplicialComplex V) : A ∈ 𝒜.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (C D C' : Finset V), cc.IsMaximal C → cc.IsMaximal D → cc.IsMaximal C' → (∀ (f : cc.Folding), ChamberComplex.OppositeSides f C D) → galleryDist cc.toSimplicialComplex C D = galleryDist cc.toSimplicialComplex C C' + galleryDist cc.toSimplicialComplex C' D
• gallery_through_chamber (C C' D : Finset V) : K.IsMaximal C → K.IsMaximal C' → K.IsMaximal D → galleryDist K.toSimplicialComplex C D = galleryDist K.toSimplicialComplex C C' + galleryDist K.toSimplicialComplex C' D → ∃ (g : Gallery K.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist K.toSimplicialComplex C D ∧ C' ∈ g.chambers

theorem wall_separates_opposite_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} {𝒜 : ApartmentSystem K} (hyp : OppositeChamberHypGen K 𝒜) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C D : Finset V) (hC : C ∈ A.faces) (hD : D ∈ A.faces) (hCmax : A.IsMaximal C) (hDmax : A.IsMaximal D) (hopp : AreOpposite K.toSimplicialComplex C D) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (f : cc.Folding) : ChamberComplex.OppositeSides f C D

Wall-separation property for opposite chambers in a spherical apartment: every folding separates them.

theorem chamber_in_minimal_gallery_of_opposite_gen {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} {𝒜 : ApartmentSystem K} (hyp : OppositeChamberHypGen K 𝒜) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C D : Finset V) (hC : C ∈ A.faces) (hD : D ∈ A.faces) (hCmax : A.IsMaximal C) (hDmax : A.IsMaximal D) (hopp : AreOpposite K.toSimplicialComplex C D) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (C' : Finset V) (hC' : C' ∈ A.faces) (hC'max : A.IsMaximal C') : ∃ (g : Gallery K.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist K.toSimplicialComplex C D ∧ C' ∈ g.chambers

Every chamber $C'$ of an apartment lies on some minimal gallery between an opposite pair $C, D$.

theorem antipodal_chambers_in_convex_hull {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) (hopp : AreOpposite K.toSimplicialComplex C D) (E : Finset V) : A.IsMaximal E → E ∈ ConvexHull K.toSimplicialComplex C D

The convex hull of antipodal (opposite) chambers is the entire apartment.

theorem face_bij_maps_maximal {V : Type u_2} [DecidableEq V] (B A : SimplicialComplex V) (ψ : V → V) (hψ_bij : Function.Bijective ψ) (hψ_faces : ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ψ s ∈ A.faces) (s : Finset V) (hs : B.IsMaximal s) : A.IsMaximal (Finset.image ψ s)

A face bijection between simplicial complexes preserves maximality.

theorem face_bij_maps_adjacent {V : Type u_2} [DecidableEq V] (B A : SimplicialComplex V) (ψ : V → V) (hψ_bij : Function.Bijective ψ) (hψ_faces : ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ψ s ∈ A.faces) (E F : Finset V) (hEF : B.Adjacent E F) : A.Adjacent (Finset.image ψ E) (Finset.image ψ F)

A face bijection between simplicial complexes preserves adjacency.

theorem isChain_map {α : Type u_2} {β : Type u_3} {R : α → α → Prop} {S : β → β → Prop} {f : α → β} (h : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (hl : List.IsChain R l) : List.IsChain S (List.map f l)

Apply a relation-respecting map to a chain to obtain a chain in the target.

theorem face_bij_gallery_le {V : Type u_2} [DecidableEq V] (B A : SimplicialComplex V) (ψ : V → V) (hψ_bij : Function.Bijective ψ) (hψ_faces : ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ψ s ∈ A.faces) (C D : Finset V) : galleryDist A (Finset.image ψ C) (Finset.image ψ D) ≤ galleryDist B C D

A face bijection between two apartments yields the inequality $d_{A'}(f(C), f(D)) \le d_A(C, D)$ between gallery distances.

theorem spherical_apt_has_opposite_pair {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (hfin : A.faces.Finite) : ∃ (C : Finset V) (D : Finset V), A.IsMaximal C ∧ A.IsMaximal D ∧ AreOpposite K.toSimplicialComplex C D

A spherical apartment has an opposite chamber pair: there exist chambers $C, D$ at maximal gallery distance.

theorem apartments_eq_of_same_chambers {V : Type u_2} [DecidableEq V] (K : ChamberComplex V) (𝒜₁ 𝒜₂ : ApartmentSystem K) (A : SimplicialComplex V) (hA₁ : A ∈ 𝒜₁.apartments) (B : SimplicialComplex V) (hB₂ : B ∈ 𝒜₂.apartments) (hchambers : ∀ (E : Finset V), A.IsMaximal E ↔ B.IsMaximal E) : A = B

Two apartments with the same set of chambers are equal.

theorem adjacent_in_subcomplex {V : Type u_1} [DecidableEq V] {A K : SimplicialComplex V} (_hsub : IsSubcomplex A K) {C D : Finset V} (hadj : K.Adjacent C D) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : A.Adjacent C D

Adjacency in $A$ follows from adjacency in $K \supseteq A$ when both chambers are maximal in $A$.

theorem chain_transfer_to_subcomplex {V : Type u_1} [DecidableEq V] {A K : SimplicialComplex V} (hsub : IsSubcomplex A K) (l : List (Finset V)) (hchain : List.IsChain K.Adjacent l) (hmax : ∀ E ∈ l, A.IsMaximal E) : List.IsChain A.Adjacent l

A chain in $K$ remains a chain in $A \subseteq K$ when all entries are maximal in $A$.

theorem galleryDist_apt_le_building {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) : galleryDist A C D ≤ galleryDist K.toSimplicialComplex C D

The gallery distance computed in an apartment is at most the gallery distance computed in the ambient building.

theorem apt_chambers_iff_convex_hull {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (𝒜 : ApartmentSystem K) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) (hopp : AreOpposite K.toSimplicialComplex C D) (_hfin : A.faces.Finite) (E : Finset V) : A.IsMaximal E ↔ E ∈ ConvexHull K.toSimplicialComplex C D

An apartment's chambers are exactly those in the convex hull of any pair of opposite chambers.