structure Building.WValuedDist {V : Type u_1} [DecidableEq V] (b : Building V) : Type (max u_1 (u_2 + 1))

The $W$-valued distance on a building: a function $\delta : \mathrm{Cham}(X)^2 \to W$ taking values in a Coxeter group $W$, with $\delta(C, C) = 1$, satisfying $\ell(\delta(C, D)) = d(C, D)$, and compatible with the natural Coxeter labeling of each apartment via an isomorphism.

• S_idx : Type u_2
• S_idx_dec : DecidableEq self.S_idx
• S_idx_fin : Fintype self.S_idx
• coxeterMatrix : CoxeterMatrix self.S_idx
• delta : Finset V → Finset V → self.coxeterMatrix.Group
• delta_self (C : Finset V) : b.IsMaximal C → self.delta C C = 1
• galleryDist_eq_length (C D : Finset V) : galleryDist b.toSimplicialComplex C D = self.coxeterMatrix.toCoxeterSystem.length (self.delta C D)
• delta_apt_compat (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) → (∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) → ∃ (iso : self.coxeterMatrix.Group ≃* M.Group), ∀ (C D : Finset V), C ∈ A.faces → A.IsMaximal C → D ∈ A.faces → A.IsMaximal D → iso (self.delta C D) = (φ C)⁻¹ * φ D

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

A retraction $\bar\rho$ onto an apartment $A$ centered at $C$ exists and preserves the $W$-valued distance from $C$ (and to $C$), fixes $A$ pointwise, and sends adjacent chambers to equal-or-adjacent chambers.

theorem Building.WValuedDist.delta_injective_in_apt {V : Type u_2} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C D₁ D₂ : Finset V) (hC_mem : C ∈ A.faces) (hC : A.IsMaximal C) (hD₁_mem : D₁ ∈ A.faces) (hD₁ : A.IsMaximal D₁) (hD₂_mem : D₂ ∈ A.faces) (hD₂ : A.IsMaximal D₂) (h_eq : δW.delta C D₁ = δW.delta C D₂) : D₁ = D₂

The $W$-valued distance from a fixed chamber $C$ is injective on chambers of any apartment containing $C$.

theorem Building.WValuedDist.folding_delta_from_center {V : Type u_2} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (ρbar : Finset V → Finset V) (hρ_max : ∀ (D : Finset V), b.IsMaximal D → ρbar D ∈ A.faces ∧ A.IsMaximal (ρbar D)) (hρ_fix : ∀ D ∈ A.faces, A.IsMaximal D → ρbar D = D) (hρ_delta : ∀ (D : Finset V), b.IsMaximal D → δW.delta C (ρbar 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 ∈ Y, δW.delta C (f y) = δW.delta C y) ∧ ∀ y ∈ Y, A.IsMaximal (f y)

Folding preserves the $W$-valued distance from the center chamber: if a folding fixes $C$, then $\delta(C, f(D)) = \delta(C, D)$ for the fold image.

theorem Building.WValuedDist.delta_retraction_agrees_with_iso {V : Type u_2} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (ρbar : Finset V → Finset V) (hρ_max : ∀ (D : Finset V), b.IsMaximal D → ρbar D ∈ A.faces ∧ A.IsMaximal (ρbar D)) (hρ_fix : ∀ D ∈ A.faces, A.IsMaximal D → ρbar D = D) (hρ_delta : ∀ (D : Finset V), b.IsMaximal D → δW.delta C (ρbar 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 → ρbar y = f y

The canonical retraction $\bar\rho$ agrees with any partial $\delta$- preserving isometry $f : Y \to A$ on its domain.

def IsStrongIsometry {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (Y Z : Set (Finset V)) (φ : Finset V → Finset V) : Prop

A strong isometry $f : Y \to f(Y)$ between sets of chambers is a bijection that preserves the $W$-valued distance $\delta$.

theorem retraction_extension_exists {V : Type u_2} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) {A : SimplicialComplex V} (hA : A ∈ b.apartmentSystem.apartments) {Y : Set (Finset V)} {f : Finset V → Finset V} (hf_strong : IsStrongIsometry δW Y (f '' Y) f) (hf_img_in_A : ∀ C ∈ Y, f C ∈ A.faces) (hY_chambers : ∀ C ∈ Y, b.IsMaximal C) {C' : Finset V} (hC'_in_A : C' ∈ A.faces) (hC'_maximal : A.IsMaximal C') (hC'_not_in_fY : C' ∉ f '' Y) (_hC'_adj : ∃ D ∈ f '' Y, A.Adjacent C' D) : ∃ (D' : Finset V), b.IsMaximal D' ∧ D' ∉ Y ∧ (∀ y ∈ Y, δW.delta (f y) C' = δW.delta y D') ∧ (∀ y ∈ Y, δW.delta C' (f y) = δW.delta D' y) ∧ δW.delta C' C' = δW.delta D' D'

Existence of a retraction extending a strong isometry $f : Y \to A$ into an apartment: the retraction agrees with $f^{-1}$ on $f(Y)$.

theorem strong_isometry_one_step_extension {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) {A : SimplicialComplex V} (hA : A ∈ b.apartmentSystem.apartments) {Y : Set (Finset V)} {f : Finset V → Finset V} (hf_strong : IsStrongIsometry δW Y (f '' Y) f) (hf_img_in_A : ∀ C ∈ Y, f C ∈ A.faces) (hY_chambers : ∀ C ∈ Y, b.IsMaximal C) {C' : Finset V} (hC'_in_A : C' ∈ A.faces) (hC'_maximal : A.IsMaximal C') (hC'_not_in_fY : C' ∉ f '' Y) (hC'_adj : ∃ D ∈ f '' Y, A.Adjacent C' D) : ∃ (g : Finset V → Finset V), IsStrongIsometry δW (f '' Y ∪ {C'}) (g '' (f '' Y ∪ {C'})) g ∧ ∀ x ∈ f '' Y, ∃ y ∈ Y, f y = x ∧ g x = y

One-step extension of a strong isometry: an adjacent chamber $C' \in A$ not yet in $f(Y)$ admits a strong-isometric extension on $f(Y) \cup \{C'\}$ agreeing with $f^{-1}$ on $f(Y)$.