def CombinatorialGeometry.MinimalGallery {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (g : Gallery K) (C D : Finset V) : Prop

A gallery $g$ is minimal between $C$ and $D$ if it connects them with length equal to the gallery distance $d(C, D)$.

def CombinatorialGeometry.ReducedGallery {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (g : Gallery K) (C D : Finset V) : Prop

A gallery is reduced if it is non-stuttering and minimal.

def CombinatorialGeometry.BuildingGalleryType {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (K : ChamberComplex V) (lab : Labelling K.toSimplicialComplex L) (g : Gallery K.toSimplicialComplex) : List (Finset L)

The label-type of a building gallery $g$ under a labelling $\mathrm{lab}$.

noncomputable def CombinatorialGeometry.WeylDistance {V : Type u_1} [DecidableEq V] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] (b : Building V) (ct : b.CoxeterTypeOfBuilding) (A : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) (φ : Finset V → ct.matrix.Group) (C D : Finset V) : ct.matrix.Group

Weyl distance $\delta_W(C, D) = (\varphi C)^{-1} \varphi D$ between chambers $C, D$ via a Coxeter-group labelling $\varphi$.

structure CombinatorialGeometry.ApartmentCharacterization {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) : Prop

Three characterizing properties of an apartment: being a subcomplex, being thin, and the property that minimal galleries starting in $A$ stay in $A$.

• sub : IsSubcomplex A b.toSimplicialComplex
• thin : ∃ (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ cc.IsThin
• minimalStaysIn (g : Gallery b.toSimplicialComplex) (C D : Finset V) : MinimalGallery b.toSimplicialComplex g C D → C ∈ A.faces → A.IsMaximal C → ∀ E ∈ g.chambers, E ∈ A.faces

def CombinatorialGeometry.PrescribedGalleryExistence {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (K : ChamberComplex V) (lab : Labelling K.toSimplicialComplex L) : Prop

$K$ has prescribed gallery existence if every chamber and label-type sequence can be realized as the gallery-type of some gallery starting at that chamber.

structure CombinatorialGeometry.PrescribedGalleryHypotheses {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

Hypotheses for the prescribed-gallery construction: existence of an apartment chain of any prescribed length, and the lift of apartment adjacency to building adjacency.

• apt_gallery_of_type (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ C ∈ A.faces, A.IsMaximal C → ∀ (τ : List (Finset V)), ∃ (cs : List (Finset V)), cs.head? = some C ∧ cs.length = τ.length + 1 ∧ (∀ E ∈ cs, E ∈ A.faces) ∧ List.IsChain A.Adjacent cs
• apt_adj_implies_bldg_adj (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (C D : Finset V), C ∈ A.faces → D ∈ A.faces → A.Adjacent C D → b.Adjacent C D

theorem CombinatorialGeometry.apt_adj_lifts_to_bldg {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C D : Finset V) (_hC : C ∈ A.faces) (_hD : D ∈ A.faces) (hadj : A.Adjacent C D) : b.Adjacent C D

Adjacency in an apartment lifts to adjacency in the ambient building.

theorem CombinatorialGeometry.apt_chain_of_length {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) (h_has_adj : ∀ (C : Finset V), A.IsMaximal C → ∃ (D : Finset V), A.Adjacent C D) (C : Finset V) (hC : C ∈ A.faces) (hCmax : A.IsMaximal C) (n : ℕ) : ∃ (cs : List (Finset V)), cs.head? = some C ∧ cs.length = n + 1 ∧ (∀ E ∈ cs, E ∈ A.faces) ∧ List.IsChain A.Adjacent cs

If every maximal chamber of $A$ has an adjacent chamber in $A$, one can build adjacency chains of any length starting at a given chamber.

theorem CombinatorialGeometry.mk_prescribed_gallery_hyp {V : Type u_1} [DecidableEq V] (b : Building V) (h_apt_has_adj : ∀ A ∈ b.apartmentSystem.apartments, ∀ (C : Finset V), A.IsMaximal C → ∃ (D : Finset V), A.Adjacent C D) : PrescribedGalleryHypotheses b

Construct PrescribedGalleryHypotheses for a building from the assumption that every apartment chamber has an adjacent chamber.