theorem building_maximal_of_apt_contains_all {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_all : ∀ s ∈ b.faces, s ∈ A.faces) {D : Finset V} (hD : b.IsMaximal D) : A.IsMaximal D

If an apartment $A$ contains every face of the building, then the building's maximal chambers are also maximal in $A$.

theorem building_adj_of_apt_contains_all {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_all : ∀ s ∈ b.faces, s ∈ A.faces) {C D : Finset V} (hadj : b.Adjacent C D) : A.Adjacent C D

Adjacency in a building transfers to adjacency in an apartment that contains all faces of the building.

theorem apt_maximal_of_building_contains_all {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_all : ∀ s ∈ b.faces, s ∈ A.faces) {D : Finset V} (hD : A.IsMaximal D) : b.IsMaximal D

Maximality in an apartment that contains all building faces lifts to maximality in the building.

theorem apt_adj_of_building_contains_all {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_all : ∀ s ∈ b.faces, s ∈ A.faces) {C D : Finset V} (hadj : A.Adjacent C D) : b.Adjacent C D

Adjacency in an apartment that contains all faces of the building lifts to adjacency in the building.

theorem canonical_BuildingRetraction {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 : b.IsMaximal C) : ∃ (ρ : BuildingRetraction b), ρ.apt = A ∧ ρ.base = C ∧ Finset.image ρ.map C = C ∧ (∀ B ∈ b.apartmentSystem.apartments, C ∈ B.faces → Function.Injective ρ.map ∧ ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ρ.map s ∈ A.faces) ∧ ∀ s ∈ b.faces, Finset.image ρ.map s = s

Existence of the canonical retraction $\rho_{D;C,A}$: for any apartment $A$ containing a chamber $C$, there is a building retraction onto $A$ centered at $C$. It is injective on any apartment $B$ containing $C$, characterizes $B$'s faces, and fixes every face of the building pointwise when the apartment contains all faces.