theorem
galleryDist_eq_coxeterLength
{V : Type u_2}
[DecidableEq V]
{b : Building V}
(δW : b.WValuedDist)
(C D : Finset V)
:
The gallery distance between two chambers $C, D$ in a building equals the Coxeter length of their $W$-valued distance $\delta(C, D)$.
theorem
delta_eq_imp_galleryDist_eq
{V : Type u_1}
[DecidableEq V]
{b : Building V}
(δW : b.WValuedDist)
(C D C' D' : Finset V)
:
δW.delta C D = δW.delta C' D' → galleryDist b.toSimplicialComplex C D = galleryDist b.toSimplicialComplex C' D'
If two pairs of chambers have the same $W$-valued distance, then they have the same gallery distance.
theorem
Building.strong_iso_ext
{V : Type u_1}
[DecidableEq V]
{b : Building V}
(δW : b.WValuedDist)
{Y : Set (Finset V)}
{A : SimplicialComplex V}
(hA : A ∈ b.apartmentSystem.apartments)
{f : Finset V → Finset V}
(hf : IsStrongIsometry δW Y (f '' Y) f)
(hf_img : ∀ C ∈ Y, f C ∈ A.faces)
:
∃ B ∈ b.apartmentSystem.apartments, ∀ C ∈ Y, C ∈ B.faces
Strong isometry extension lemma: any strong isometry $f : Y \to A$ from a set of chambers $Y$ into an apartment $A$ extends to an apartment $B$ containing $Y$. This is the key technical lemma underlying the existence of a maximal apartment system (Section 15.5).