structure Labelling {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (L : Type u_2) [DecidableEq L] : Type (max u_1 u_2)

A labelling of a simplicial complex $K$ by a set $L$: a strict-monotone assignment of a finite, nonempty set of labels to each face, monotone with respect to face inclusion.

• labelMap : Finset V → Finset L
• label_nonempty (s : Finset V) : s ∈ K.faces → (self.labelMap s).Nonempty
• label_strictMono (s t : Finset V) : s ∈ K.faces → t ∈ K.faces → s ⊂ t → self.labelMap s ⊂ self.labelMap t

def SimplicialComplex.IsLabellable {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) : Prop

A simplicial complex $K$ is labellable if there exists a labelling by some label type.

def Labelling.labelOf {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {L : Type u_2} [DecidableEq L] (lab : Labelling K L) (s : Finset V) : Finset L

Application of a labelling to a face: returns the label set assigned to $s$.

def LabelAdjacent {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (K : ChamberComplex V) (lab : Labelling K.toSimplicialComplex L) (ℓ : Finset L) (C₁ C₂ : Finset V) : Prop

Two chambers $C_1, C_2$ are $\ell$-adjacent (with respect to a labelling) if they are adjacent and the label of their common face $C_1 \cap C_2$ equals $\ell$.

def ChamberComplex.IsUniquelyLabellable {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

A chamber complex is uniquely labellable if any two labellings differ by a bijection of label sets, i.e. all labellings are canonical up to renaming of labels.

def SimplicialComplex.link {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (_hσ : σ ∈ K.faces) : Set (Finset V)

The link of a face $\sigma$ in $K$: the set of nonempty faces $\tau$ disjoint from $\sigma$ such that $\sigma \cup \tau$ is still a face of $K$.

theorem mem_of_getLast?_eq {α : Type u_2} {l : List α} {a : α} (h : l.getLast? = some a) : a ∈ l

If l.getLast? = some a, then $a$ is a member of $l$.

theorem label_agree_along_chain {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {L₁ : Type u_2} {L₂ : Type u_3} [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling K L₁) (lab₂ : Labelling K L₂) (f : L₁ → L₂) (hadj_prop : ∀ (C₁ C₂ : Finset V), K.Adjacent C₁ C₂ → lab₂.labelMap C₁ = Finset.image f (lab₁.labelMap C₁) → lab₂.labelMap C₂ = Finset.image f (lab₁.labelMap C₂)) (cs : List (Finset V)) (hne : cs ≠ []) (hchain : List.IsChain K.Adjacent cs) (hagree : lab₂.labelMap (cs.head hne) = Finset.image f (lab₁.labelMap (cs.head hne))) (D : Finset V) : D ∈ cs → lab₂.labelMap D = Finset.image f (lab₁.labelMap D)

Label agreement propagates along a chain of adjacent chambers: if two labellings $\mathrm{lab}_1$ and $\mathrm{lab}_2$ are related by a function $f$ on the head of a chain and the relation passes through adjacency, then the relation holds along the whole chain.

theorem label_agree_all_chambers {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} {L₁ : Type u_2} {L₂ : Type u_3} [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling K.toSimplicialComplex L₁) (lab₂ : Labelling K.toSimplicialComplex L₂) (f : L₁ → L₂) (hadj_prop : ∀ (C₁ C₂ : Finset V), K.Adjacent C₁ C₂ → lab₂.labelMap C₁ = Finset.image f (lab₁.labelMap C₁) → lab₂.labelMap C₂ = Finset.image f (lab₁.labelMap C₂)) (C₀ : Finset V) (hC₀ : K.IsMaximal C₀) (hagree₀ : lab₂.labelMap C₀ = Finset.image f (lab₁.labelMap C₀)) (D : Finset V) : K.IsMaximal D → lab₂.labelMap D = Finset.image f (lab₁.labelMap D)

Label agreement at one chamber propagates to all chambers via the gallery-connectedness of a chamber complex.

theorem label_agree_all_faces {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} {L₁ : Type u_2} {L₂ : Type u_3} [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling K.toSimplicialComplex L₁) (lab₂ : Labelling K.toSimplicialComplex L₂) (f : L₁ → L₂) (hadj_prop : ∀ (C₁ C₂ : Finset V), K.Adjacent C₁ C₂ → lab₂.labelMap C₁ = Finset.image f (lab₁.labelMap C₁) → lab₂.labelMap C₂ = Finset.image f (lab₁.labelMap C₂)) (hsub_prop : ∀ (C : Finset V), K.IsMaximal C → lab₂.labelMap C = Finset.image f (lab₁.labelMap C) → ∀ s ∈ K.faces, s ⊆ C → lab₂.labelMap s = Finset.image f (lab₁.labelMap s)) (C₀ : Finset V) (hC₀ : K.IsMaximal C₀) (hagree₀ : lab₂.labelMap C₀ = Finset.image f (lab₁.labelMap C₀)) (s : Finset V) : s ∈ K.faces → lab₂.labelMap s = Finset.image f (lab₁.labelMap s)

Label agreement at one chamber propagates to all faces via gallery-connectedness on chambers together with downward propagation from each chamber to its subfaces.

theorem building_has_chamber {V : Type u_2} [DecidableEq V] (b : Building V) : ∃ (C : Finset V), b.IsMaximal C

Every building has at least one chamber, extracted from a nonempty apartment.

theorem building_label_translation {V : Type u_2} [DecidableEq V] (b : Building V) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling b.toSimplicialComplex L₁) (lab₂ : Labelling b.toSimplicialComplex L₂) (C₀ : Finset V) (hC₀ : b.IsMaximal C₀) : ∃ (f : L₁ → L₂), Function.Bijective f ∧ lab₂.labelMap C₀ = Finset.image f (lab₁.labelMap C₀)

For two labellings of a building, on any fixed chamber there exists a bijection $f$ between the two label types translating one labelling into the other.

theorem building_adj_label_propagation {V : Type u_2} [DecidableEq V] (b : Building V) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling b.toSimplicialComplex L₁) (lab₂ : Labelling b.toSimplicialComplex L₂) (f : L₁ → L₂) (hf_bij : Function.Bijective f) (C₁ C₂ : Finset V) (hadj : b.Adjacent C₁ C₂) (hagree : lab₂.labelMap C₁ = Finset.image f (lab₁.labelMap C₁)) : lab₂.labelMap C₂ = Finset.image f (lab₁.labelMap C₂)

Adjacency-step propagation of label agreement across a building: a bijection $f$ relating the labels on a chamber $C_1$ extends to the labels on any adjacent chamber $C_2$.

theorem building_subface_label_propagation {V : Type u_2} [DecidableEq V] (b : Building V) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Labelling b.toSimplicialComplex L₁) (lab₂ : Labelling b.toSimplicialComplex L₂) (f : L₁ → L₂) (hf_bij : Function.Bijective f) (C : Finset V) (hC : b.IsMaximal C) (hagree : lab₂.labelMap C = Finset.image f (lab₁.labelMap C)) (s : Finset V) (hs : s ∈ b.faces) (hsC : s ⊆ C) : lab₂.labelMap s = Finset.image f (lab₁.labelMap s)

Subface propagation of label agreement: if a bijection relates the labels on a chamber $C$, then it also relates the labels on every subface $s \subseteq C$.