noncomputable def retraction_map {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_max : A.IsMaximal C) : V → V

The canonical retraction map $\rho : V \to V$ obtained from exists_canonical_retraction.

theorem retraction_map_face {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_max : A.IsMaximal C) (s : Finset V) : s ∈ b.faces → Finset.image (retraction_map b A hA C hC_A hC_max) s ∈ A.faces

The retraction map sends faces of the building to faces of the chosen apartment $A$.

theorem retraction_map_fixes_apt {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_max : A.IsMaximal C) (v : V) : (∃ s ∈ A.faces, v ∈ s) → retraction_map b A hA C hC_A hC_max v = v

The retraction map fixes every vertex lying in the apartment $A$.

theorem retraction_map_injective_on_apt {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_max : A.IsMaximal C) (B : SimplicialComplex V) : B ∈ b.apartmentSystem.apartments → C ∈ B.faces → ∀ (v₁ v₂ : V), (∃ s ∈ B.faces, v₁ ∈ s) → (∃ s ∈ B.faces, v₂ ∈ s) → retraction_map b A hA C hC_A hC_max v₁ = retraction_map b A hA C hC_A hC_max v₂ → v₁ = v₂

The retraction map is injective on the vertices of any apartment $B$ containing $C$.

theorem retraction_restricts_to_simplicial_map_A'_to_A {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max : A.IsMaximal C) (s : Finset V) : s ∈ A'.faces → Finset.image (retraction_map b A hA C hC_A hC_max) s ∈ A.faces

The retraction restricted to a second apartment $A'$ sends faces of $A'$ into faces of $A$.

theorem retraction_injective_on_apt_vertices {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max : A.IsMaximal C) (v₁ v₂ : V) : (∃ s ∈ A'.faces, v₁ ∈ s) → (∃ s ∈ A'.faces, v₂ ∈ s) → retraction_map b A hA C hC_A hC_max v₁ = retraction_map b A hA C hC_A hC_max v₂ → v₁ = v₂

Specialization of injectivity of the retraction to vertices of another apartment $A'$.

theorem retraction_image_ssubset_of_ssubset {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max : A.IsMaximal C) (s t : Finset V) (hs : s ∈ A'.faces) (ht : t ∈ A'.faces) (hst : s ⊂ t) : Finset.image (retraction_map b A hA C hC_A hC_max) s ⊂ Finset.image (retraction_map b A hA C hC_A hC_max) t

Strict monotonicity of the retraction-induced image map on faces of $A'$.

theorem retraction_identity_on_apt {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max_bldg : b.IsMaximal C) (s : Finset V) : s ∈ A'.faces → Finset.image (retraction_map b A hA C hC_A ⋯) s = s

The retraction $\rho$ centered at a chamber $C$ acts as the identity on every face of any apartment $A'$ also containing $C$ — a consequence of label-uniqueness.

theorem apt_faces_subset {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max_bldg : b.IsMaximal C) : A'.faces ⊆ A.faces

Apartments containing a common chamber $C$ have one face-set contained in the other; in particular this yields $A'.\mathrm{faces} \subseteq A.\mathrm{faces}$.

theorem apt_iso_exists_fixing_intersection {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max : b.IsMaximal C) : ∃ (φ : V → V), (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ s ∈ A'.faces, v ∈ s) → φ v = v) ∧ Function.Bijective φ

Section 4.1 / 4.4: between two apartments $A, A'$ sharing a chamber $C$ there exists a simplicial isomorphism $\varphi : V \to V$ that is bijective and fixes the intersection $A \cap A'$ pointwise.