theorem SimplicialComplex.sdiff_union_eq_sdiff_of_disjoint' {V : Type} [DecidableEq V] {σ F τ : Finset V} (_hF_disj : Disjoint σ F) (hτ_disj : Disjoint σ τ) : (σ ∪ τ) \ (σ ∪ F) = τ \ F

When $\tau$ is disjoint from $\sigma$, the set difference $(\sigma \cup \tau) \setminus (\sigma \cup F)$ equals $\tau \setminus F$.

theorem SimplicialComplex.union_maximal_of_linkComplex_maximal' {V : Type} [DecidableEq V] {K : SimplicialComplex V} {σ : Finset V} (hσ : σ ∈ K.faces) {τ : Finset V} (hτ_max : (K.linkComplex σ hσ).IsMaximal τ) : K.IsMaximal (σ ∪ τ)

A maximal face $\tau$ of the link $\mathrm{lk}_K(\sigma)$ lifts to a maximal face $\sigma \cup \tau$ of the ambient complex $K$.

theorem SimplicialComplex.linkComplex_maximal_of_union_maximal' {V : Type} [DecidableEq V] {K : SimplicialComplex V} {σ : Finset V} (hσ : σ ∈ K.faces) {τ : Finset V} (hτ_link : τ ∈ (K.linkComplex σ hσ).faces) (hστ_max : K.IsMaximal (σ ∪ τ)) : (K.linkComplex σ hσ).IsMaximal τ

The converse direction: if $\sigma \cup \tau$ is maximal in $K$ and $\tau$ lies in the link of $\sigma$, then $\tau$ is maximal in $\mathrm{lk}_K(\sigma)$.

theorem SimplicialComplex.linkComplex_sub {V : Type} [DecidableEq V] {K A : SimplicialComplex V} (hA : IsSubcomplex A K) (σ : Finset V) (hσK : σ ∈ K.faces) (hσA : σ ∈ A.faces) : IsSubcomplex (A.linkComplex σ hσA) (K.linkComplex σ hσK)

The link operation is monotone with respect to subcomplex inclusion: if $A$ is a subcomplex of $K$, then $\mathrm{lk}_A(\sigma)$ is a subcomplex of $\mathrm{lk}_K(\sigma)$.

theorem link_exists_maximal {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (s : Finset V) : s ∈ (b.linkComplex σ hσ).faces → ∃ (C : Finset V), (b.linkComplex σ hσ).IsMaximal C ∧ s ⊆ C

Every face of the link $\mathrm{lk}_K(\sigma)$ extends to a maximal face of the link, witnessed by extending a chamber of $K$ containing $\sigma \cup s$ and removing $\sigma$.

theorem iso_exists_injective {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (B : SimplicialComplex V) (hB : B ∈ b.apartmentSystem.apartments) (x : Finset V) (hxA : x ∈ A.faces) (hxB : x ∈ B.faces) (C : Finset V) (hC_max : A.IsMaximal C) (hCB : C ∈ B.faces) (φ : SimplicialMap A B) (hφ_fix_x : ∀ v ∈ x, φ.toFun v = v) (hφ_fix_C : ∀ v ∈ C, φ.toFun v = v) (v₁ v₂ : V) : (∃ s ∈ A.faces, v₁ ∈ s) → (∃ s ∈ A.faces, v₂ ∈ s) → φ.toFun v₁ = φ.toFun v₂ → v₁ = v₂

An apartment isomorphism $\varphi : A \to B$ fixing a chamber $C$ pointwise (and a face $x$ pointwise) is injective on the vertex set covered by faces of $A$, by reduction to the unique labelling property.

theorem link_iso_exists {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A' : SimplicialComplex V) : A' ∈ link_apts → ∀ B' ∈ link_apts, ∀ x ∈ A'.faces, x ∈ B'.faces → ∀ (C : Finset V), A'.IsMaximal C → C ∈ B'.faces → ∃ (φ : SimplicialMap A' B'), (∀ v ∈ x, φ.toFun v = v) ∧ ∀ v ∈ C, φ.toFun v = v

Isomorphism axiom for link apartments: given link apartments $A', B'$ sharing a face $x$ and a chamber $C \subseteq A' \cap B'$ with $A'.IsMaximal C$, an ambient apartment isomorphism restricts to an isomorphism of link apartments fixing $x$ and $C$.

theorem link_maximal_in_apt_is_maximal {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∀ (C : Finset V), A.IsMaximal C → (b.linkComplex σ hσ).IsMaximal C

A maximal face of a link apartment is also maximal in the link of the whole building, by lifting through the ambient apartment structure.

theorem link_gallery_dist_le {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_cc : ChamberComplex V) (h_link_cc : link_cc.toSimplicialComplex = b.linkComplex σ hσ) (C D : Finset V) (hC_max : (b.linkComplex σ hσ).IsMaximal C) (hD_max : (b.linkComplex σ hσ).IsMaximal D) : galleryDist link_cc.toSimplicialComplex C D ≤ galleryDist b.toSimplicialComplex (σ ∪ C) (σ ∪ D)

Gallery distance in the link is bounded by the gallery distance of the lifted chambers in the ambient building: $d_{\mathrm{lk}}(C, D) \leq d_K(\sigma \cup C, \sigma \cup D)$.

theorem link_gallery_convex {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_cc : ChamberComplex V) (h_link_cc : link_cc.toSimplicialComplex = b.linkComplex σ hσ) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∀ (C D : Finset V), C ∈ A.faces → link_cc.IsMaximal C → D ∈ A.faces → link_cc.IsMaximal D → ∀ (g : Gallery link_cc.toSimplicialComplex), g.Connects C D → g.length = galleryDist link_cc.toSimplicialComplex C D → ∀ E ∈ g.chambers, E ∈ A.faces

Gallery convexity axiom for link apartments: any minimal gallery in the link between two chambers of a link apartment $A$ stays entirely inside $A$, proven by lifting the gallery to the ambient building and applying ambient gallery convexity.

theorem link_building_maximal_in_apt_is_apt_maximal {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∀ C ∈ A.faces, (b.linkComplex σ hσ).IsMaximal C → A.IsMaximal C

A face that is globally maximal in the link and lies in a link apartment $A$ is also maximal inside $A$ as a link apartment.

theorem link_apt_nonempty {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∃ (s : Finset V), s ∈ A.faces

Every link apartment is nonempty: it contains $C \setminus \sigma$ for any chamber $C$ of the ambient apartment that strictly contains $\sigma$.

theorem link_iso_bijective {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∀ A' ∈ link_apts, ∀ C ∈ A.faces, C ∈ A'.faces → A.IsMaximal C → ∃ (φ : V → V), Function.Bijective φ ∧ ∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces

Bijectivity of link apartment isomorphisms: for two link apartments sharing a chamber $C$, there is a bijection $\varphi : V \to V$ inducing an isomorphism between them, obtained from the ambient apartment isomorphism that fixes $\sigma \cup C$.

theorem link_of_coxeter_complex_is_coxeter {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (σ : Finset V) (hσ : σ ∈ A.faces) (hσ_proper : ∃ (C : Finset V), A.IsMaximal C ∧ σ ⊂ C) : ∃ (B_idx' : Type) (M' : CoxeterMatrix B_idx') (cc' : ChamberComplex V), cc'.toSimplicialComplex = A.linkComplex σ hσ ∧ ∃ (φ' : Finset V → M'.Group), (∀ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C → ∀ (D : Finset V), (A.linkComplex σ hσ).IsMaximal D → φ' C = φ' D → C = D) ∧ (∀ (w : M'.Group), ∃ (C : Finset V), (A.linkComplex σ hσ).IsMaximal C ∧ φ' C = w) ∧ (∀ (C C' : Finset V), (A.linkComplex σ hσ).Adjacent C C' → CoxeterComplex.ChamberAdjacent M' (φ' C) (φ' C')) ∧ cc'.IsThin

The link of a face $\sigma$ in a Coxeter complex carries a natural Coxeter complex structure on a (smaller) Coxeter system $M'$, realising the parabolic subgroup associated to $\sigma$.

theorem link_apt_is_coxeter {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (A : SimplicialComplex V) : A ∈ link_apts → ∃ (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ ∃ (φ : 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) ∧ (∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) ∧ cc.IsThin

Each link apartment is itself a Coxeter complex, obtained by applying link_of_coxeter_complex_is_coxeter to the ambient apartment's Coxeter structure.

theorem coxeter_complex_unique_labelling' {V : Type} [DecidableEq V] (A : SimplicialComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hadj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) : (∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) → (∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) → ∀ (C₀ : Finset V), A.IsMaximal C₀ → (∃ (f : L₁ → L₂), Function.Bijective f ∧ lab₂ C₀ = Finset.image f (lab₁ C₀)) ∧ ∀ (f : L₁ → L₂), Function.Bijective f → lab₂ C₀ = Finset.image f (lab₁ C₀) → ∀ s ∈ A.faces, lab₂ s = Finset.image f (lab₁ s)

Unique labelling property for Coxeter complexes: any two labelings of $A$ that agree on a fixed chamber $C_0$ (up to a bijection of labels) agree on every face, with existence and uniqueness of the bijection.

theorem Building.link_contains_pair {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (link_apts : Set (SimplicialComplex V)) (h_link_apts : link_apts = {L : SimplicialComplex V | ∃ A ∈ b.apartmentSystem.apartments, ∃ (hσA : σ ∈ A.faces), L = A.linkComplex σ hσA}) (C' D' : Finset V) (hC'_max : (b.linkComplex σ hσ).IsMaximal C') (hD'_max : (b.linkComplex σ hσ).IsMaximal D') : ∃ A ∈ link_apts, C' ∈ A.faces ∧ D' ∈ A.faces

Any two chambers $C', D'$ of the link both lie in a common link apartment, obtained from an ambient apartment containing the lifted chambers $\sigma \cup C'$ and $\sigma \cup D'$.

theorem Building.link_is_thick {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (F' C' : Finset V) : (b.linkComplex σ hσ).IsFacet F' C' → (b.linkComplex σ hσ).IsMaximal C' → ∃ (D₁ : Finset V) (D₂ : Finset V), D₁ ≠ C' ∧ D₂ ≠ C' ∧ D₁ ≠ D₂ ∧ (b.linkComplex σ hσ).IsFacet F' D₁ ∧ (b.linkComplex σ hσ).IsMaximal D₁ ∧ (b.linkComplex σ hσ).IsFacet F' D₂ ∧ (b.linkComplex σ hσ).IsMaximal D₂

Thickness of the link: every facet $F'$ of the link is contained in at least three distinct chambers, deduced from thickness of the ambient building applied to $\sigma \cup F'$.

theorem Building.link_gallery_connected {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (C D : Finset V) : (b.linkComplex σ hσ).IsMaximal C → (b.linkComplex σ hσ).IsMaximal D → ∃ (g : Gallery (b.linkComplex σ hσ)), g.chambers.head? = some C ∧ g.chambers.getLast? = some D

Gallery-connectedness of the link: any two chambers of the link are joined by a gallery, obtained by transporting a gallery from a common Coxeter link apartment back to the link complex.

noncomputable def Building.link_building {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) : Building V

The link building: the link $\mathrm{lk}_K(\sigma)$ of a face $\sigma$ of a building, equipped with the apartment system consisting of links of ambient apartments, is itself a building.