theorem CombinatorialGeometry.auxiliary_retraction_exists {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) : ∃ (ρ : Finset V → Finset V), (∀ (D : Finset V), b.IsMaximal D → ρ D ∈ A.faces ∧ A.IsMaximal (ρ D)) ∧ (∀ D ∈ A.faces, A.IsMaximal D → ρ D = D) ∧ (∀ (D : Finset V), b.IsMaximal D → δW.delta C (ρ D) = δW.delta C D) ∧ (∀ (D : Finset V), b.IsMaximal D → δW.delta (ρ D) C = δW.delta D C) ∧ ∀ (D₁ D₂ : Finset V), b.Adjacent D₁ D₂ → ρ D₁ = ρ D₂ ∨ A.Adjacent (ρ D₁) (ρ D₂)

Existence of an auxiliary retraction $\rho$ onto an apartment $A$ centered at $C$ that preserves the Weyl-valued distance $\delta_W(C, \cdot)$ and sends adjacent chambers to equal or adjacent images.

theorem CombinatorialGeometry.strong_isometry_determined_by_retraction {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (ρ : Finset V → Finset V) (hρ_max : ∀ (D : Finset V), b.IsMaximal D → ρ D ∈ A.faces ∧ A.IsMaximal (ρ D)) (hρ_fix : ∀ D ∈ A.faces, A.IsMaximal D → ρ D = D) (hρ_delta : ∀ (D : Finset V), b.IsMaximal D → δW.delta C (ρ D) = δW.delta C D) (Y : Set (Finset V)) (f : Finset V → Finset V) (hY : ∀ y ∈ Y, b.IsMaximal y) (hf_img : ∀ y ∈ Y, f y ∈ A.faces) (hf_delta : ∀ y₁ ∈ Y, ∀ y₂ ∈ Y, δW.delta (f y₁) (f y₂) = δW.delta y₁ y₂) (y : Finset V) : y ∈ Y → ρ y = f y

The Weyl-distance preserving retraction agrees with any other $\delta_W$-isometry $f$ on the domain $Y$ where $f$ takes values in $A$.