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

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

theorem AffineBuilding.coxeter_wall_crossing_gallery_dist {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (eta : Wall b) (_heta_apt : eta.apartment = A') (C_meet : Finset V) (_hC_meet_face : C_meet ∈ A'.faces) (_hC_meet_max : A'.IsMaximal C_meet) (_hC_meet_pos : ∀ v ∈ C_meet, v ∈ eta.halfPos) (D₀ : Finset V) (_hD₀_face : D₀ ∈ A'.faces) (_hD₀_max : A'.IsMaximal D₀) (_hD₀_pos : ∃ v ∈ D₀, v ∈ eta.halfPos) (D' : Finset V) (_hD'_face : D' ∈ A'.faces) (_hD'_max : A'.IsMaximal D') (_hD'_neg : ∃ v ∈ D', v ∈ eta.halfNeg) (F : Finset V) (_hF_face : F ∈ A'.faces) (_hF_sub_D₀ : F ⊆ D₀) (_hF_sub_D' : F ⊆ D') : galleryDist A' C_meet D' = galleryDist A' C_meet D₀ + 1

Crossing a wall $\eta$ from a chamber $D_0$ in $\eta^+$ to a chamber $D'$ in $\eta^-$ across a face $F$ increases the gallery distance to $C_{\text{meet}}$ by exactly one.

theorem AffineBuilding.reduced_type_gallery_replacement {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (C_meet : Finset V) (_hC_meet_face : C_meet ∈ A'.faces) (_hC_meet_max : A'.IsMaximal C_meet) (D₀ : Finset V) (_hD₀_face : D₀ ∈ A'.faces) (_hD₀_max : A'.IsMaximal D₀) (D : Finset V) (_hD_face : D ∈ A'.faces) (_hD_max : A'.IsMaximal D) (F : Finset V) (_hF_face : F ∈ A'.faces) (_hF_sub_D₀ : F ⊆ D₀) (_hF_sub_D : F ⊆ D) (D' : Finset V) (_hD'_face : D' ∈ A'.faces) (_hD'_max : A'.IsMaximal D') (_hF_sub_D' : F ⊆ D') (_h_dist_D' : galleryDist A' C_meet D' = galleryDist A' C_meet D₀ + 1) : galleryDist A' C_meet D = galleryDist A' C_meet D₀ + 1

Replacement principle: any chamber $D$ adjacent to $D_0$ across the same face $F$ inherits the same gallery distance relation to $C_{\text{meet}}$ as $D'$.

theorem AffineBuilding.gallery_dist_wall_extension {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (eta : Wall b) (_heta_apt : eta.apartment = A') (C_meet : Finset V) (_hC_meet_face : C_meet ∈ A'.faces) (_hC_meet_max : A'.IsMaximal C_meet) (_hC_meet_pos : ∀ v ∈ C_meet, v ∈ eta.halfPos) (D₀ : Finset V) (_hD₀_face : D₀ ∈ A'.faces) (_hD₀_max : A'.IsMaximal D₀) (_hD₀_pos : ∃ v ∈ D₀, v ∈ eta.halfPos) (D : Finset V) (_hD_face : D ∈ A'.faces) (_hD_max : A'.IsMaximal D) (F : Finset V) (_hF_face : F ∈ A'.faces) (_hF_sub_D₀ : F ⊆ D₀) (_hF_sub_D : F ⊆ D) (D' : Finset V) (_hD'_face : D' ∈ A'.faces) (_hD'_max : A'.IsMaximal D') (_hD'_neg : ∃ v ∈ D', v ∈ eta.halfNeg) (_hF_sub_D' : F ⊆ D') : galleryDist A' C_meet D = galleryDist A' C_meet D₀ + 1 ∧ galleryDist A' C_meet D' = galleryDist A' C_meet D₀ + 1

Combination of coxeter_wall_crossing_gallery_dist and reduced_type_gallery_replacement: both $D$ and $D'$ are at distance $\text{dist}(C_{\text{meet}}, D_0) + 1$.

theorem AffineBuilding.intersection_fixing_map_is_identity {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (ρ : SimplicialMap A' A) (hρ_fix : ∀ (v : V), (∃ s ∈ A'.faces, v ∈ s) → (∃ t ∈ A.faces, v ∈ t) → ρ.toFun v = v) (s : Finset V) (hs : s ∈ A'.faces) : Finset.image ρ.toFun s = s

A simplicial map $A' → A$ between apartments that fixes the intersection pointwise acts as the identity on every simplex of $A'$ — basically AptIsoFixesIntersection.

theorem AffineBuilding.galleryDist_of_faces_eq {V : Type} [DecidableEq V] (A A' : SimplicialComplex V) (h_sub : A'.faces ⊆ A.faces) (h_sup : A.faces ⊆ A'.faces) (X Y : Finset V) : galleryDist A X Y = galleryDist A' X Y

Gallery distance is invariant under apartments with the same face set.

theorem AffineBuilding.sector_retraction_preserves_gallery_dist {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (S : Sector b) (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (ρ : SimplicialMap A' S.apartment) (_hρ_fix : ∀ (v : V), (∃ s ∈ A'.faces, v ∈ s) → (∃ t ∈ S.apartment.faces, v ∈ t) → ρ.toFun v = v) (X Y : Finset V) (_hX_face : X ∈ A'.faces) (_hX_max : A'.IsMaximal X) (_hY_face : Y ∈ A'.faces) (_hY_max : A'.IsMaximal Y) : galleryDist S.apartment (Finset.image ρ.toFun X) (Finset.image ρ.toFun Y) = galleryDist A' X Y

The retraction of an apartment $A'$ onto a sector's apartment along $S$ preserves the gallery distance between two chambers $X, Y$ of $A'$.

theorem AffineBuilding.gallery_retraction_nonstuttering {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (S : Sector b) (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (ρ : SimplicialMap A' S.apartment) (_hρ_fix : ∀ (v : V), (∃ s ∈ A'.faces, v ∈ s) → (∃ t ∈ S.apartment.faces, v ∈ t) → ρ.toFun v = v) (eta : Wall b) (_heta_apt : eta.apartment = A') (C_meet : Finset V) (_hC_meet_face : C_meet ∈ A'.faces) (_hC_meet_max : A'.IsMaximal C_meet) (_hC_meet_pos : ∀ v ∈ C_meet, v ∈ eta.halfPos) (D₀ : Finset V) (_hD₀_face : D₀ ∈ A'.faces) (_hD₀_max : A'.IsMaximal D₀) (_hD₀_pos : ∃ v ∈ D₀, v ∈ eta.halfPos) (D : Finset V) (_hD_face : D ∈ A'.faces) (_hD_max : A'.IsMaximal D) (F : Finset V) (_hF_face : F ∈ A'.faces) (_hF_sub_D₀ : F ⊆ D₀) (_hF_sub_D : F ⊆ D) (D' : Finset V) (_hD'_face : D' ∈ A'.faces) (_hD'_max : A'.IsMaximal D') (_hD'_neg : ∃ v ∈ D', v ∈ eta.halfNeg) (_hF_sub_D' : F ⊆ D') : Finset.image ρ.toFun D ≠ Finset.image ρ.toFun D₀ ∧ Finset.image ρ.toFun D' ≠ Finset.image ρ.toFun D₀

The sector retraction is non-stuttering: chambers $D, D'$ on opposite sides of the wall $\eta$ are mapped to distinct chambers from $D_0$.

theorem AffineBuilding.simplicial_map_apt_preserves_maximal {V : Type} [DecidableEq V] {b : Building V} (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (A : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) (ρ : SimplicialMap A' A) (C : Finset V) (_hC : C ∈ A'.faces) (_hC_max : A'.IsMaximal C) : A.IsMaximal (Finset.image ρ.toFun C)

Simplicial maps between apartments preserve maximal faces (chambers).

theorem AffineBuilding.retraction_image_properties {V : Type} [DecidableEq V] {b : Building V} (A' : SimplicialComplex V) (_hA' : A' ∈ b.apartmentSystem.apartments) (A : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) (ρ : SimplicialMap A' A) (D₀ : Finset V) (_hD₀ : D₀ ∈ A'.faces) (_hD₀_max : A'.IsMaximal D₀) (D : Finset V) (_hD : D ∈ A'.faces) (_hD_max : A'.IsMaximal D) (D' : Finset V) (_hD' : D' ∈ A'.faces) (_hD'_max : A'.IsMaximal D') (F : Finset V) (_hF : F ∈ A'.faces) (_hF_sub_D₀ : F ⊆ D₀) (_hF_sub_D : F ⊆ D) (_hF_sub_D' : F ⊆ D') : A.IsMaximal (Finset.image ρ.toFun D₀) ∧ A.IsMaximal (Finset.image ρ.toFun D) ∧ A.IsMaximal (Finset.image ρ.toFun D') ∧ Finset.image ρ.toFun F ∈ A.faces

Under a simplicial map between apartments, chambers map to chambers and faces to faces — a packaged convenience lemma.