structure BuildingRetraction {V : Type u_1} [DecidableEq V] (b : Building V) : Type u_1

A retraction $\rho_{D;C,A} : X \to A$ of a building $X$ onto an apartment $A$ centered at a chamber $C$ (the base): a simplicial map fixing $A$ pointwise, sending each chamber of $X$ to a chamber of $A$, and preserving adjacency up to collapse.

• apt : SimplicialComplex V
• apt_mem : self.apt ∈ b.apartmentSystem.apartments
• base : Finset V
• base_maximal : self.apt.IsMaximal self.base
• map : V → V
• map_face (s : Finset V) : s ∈ b.faces → Finset.image self.map s ∈ self.apt.faces
• map_fixes (v : V) : (∃ s ∈ self.apt.faces, v ∈ s) → self.map v = v
• map_chamber (C : Finset V) : b.IsMaximal C → self.apt.IsMaximal (Finset.image self.map C)
• map_adj_or_eq (C D : Finset V) : b.Adjacent C D → Finset.image self.map C = Finset.image self.map D ∨ self.apt.Adjacent (Finset.image self.map C) (Finset.image self.map D)

def BuildingRetraction.IsDistanceDiminishing {V : Type u_1} [DecidableEq V] {b : Building V} (ρ : BuildingRetraction b) : Prop

A building retraction is distance-diminishing if for any two chambers $C, D$ of $X$, the gallery distance in $A$ from $\rho(C)$ to $\rho(D)$ is at most the gallery distance from $C$ to $D$ in $X$.