def IsLabelPreservingMap {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (b : Building V) (A : SimplicialComplex V) (lab : Labelling b.toSimplicialComplex L) (φ : V → V) : Prop

A map $\varphi : V \to V$ is label-preserving on apartment $A$ relative to a given labelling $\mathrm{lab}$ if it preserves the label of every face of $A$.

def IsUniversallyLabelPreserving {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (φ : V → V) : Prop

A map $\varphi : V \to V$ is universally label-preserving on $A$ if it is label-preserving relative to every labelling of the building.

theorem apt_iso_fixing_intersection_is_label_preserving {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) (_hφ_face : ∀ s ∈ A.faces, Finset.image φ s ∈ A'.faces) (hφ_fixes : ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ s ∈ A'.faces, v ∈ s) → φ v = v) (L : Type) [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) (s : Finset V) : s ∈ A.faces → lab.labelMap (Finset.image φ s) = lab.labelMap s

An apartment isomorphism that fixes the intersection of two apartments $A \cap A'$ (containing some common chamber $C$) is automatically label-preserving on $A$ for every labelling: such a map acts as the identity on every face of $A$.

theorem apt_iso_label_preserving {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 ∈ A.faces, Finset.image φ s ∈ A'.faces) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ s ∈ A'.faces, v ∈ s) → φ v = v) ∧ Function.Bijective φ ∧ ∀ (L : Type) [inst : DecidableEq L] (lab : Labelling b.toSimplicialComplex L), ∀ s ∈ A.faces, lab.labelMap (Finset.image φ s) = lab.labelMap s) ∧ ∀ (φ : V → V), (∀ s ∈ A.faces, Finset.image φ s ∈ A'.faces) → (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ s ∈ A'.faces, v ∈ s) → φ v = v) → ∀ (L : Type) [inst : DecidableEq L] (lab : Labelling b.toSimplicialComplex L), ∀ s ∈ A.faces, lab.labelMap (Finset.image φ s) = lab.labelMap s

Existence and universality of label-preserving apartment isomorphisms: for any two apartments $A, A'$ sharing a common chamber $C$, there is a bijection $\varphi$ that fixes $A \cap A'$ and is label-preserving for every labelling; moreover every such $\varphi$ is label-preserving.