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

If $\tau$ is a maximal face of the link $\mathrm{lk}_K(\sigma)$, then $\sigma \cup \tau$ is a maximal face of the ambient complex $K$.

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

Any two chambers $C, D$ of an apartment $A$ are related by a bijective automorphism of $A$ sending $D$ to $C$.

theorem finset_image_ssubset_of_injective' {V : Type} [DecidableEq V] {f : V → V} (hf : Function.Injective f) {s t : Finset V} (h : s ⊂ t) : Finset.image f s ⊂ Finset.image f t

Pushing forward a strict inclusion of finite sets along an injective map yields a strict inclusion of images.

theorem bijective_face_iso_preserves_maximal' {V : Type} [DecidableEq V] {A A' : SimplicialComplex V} {φ : V → V} (hφ_bij : Function.Bijective φ) (hφ_faces : ∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces) {s : Finset V} (hs : A.IsMaximal s) : A'.IsMaximal (Finset.image φ s)

A bijective simplicial isomorphism $\varphi : A \to A'$ carries maximal faces of $A$ to maximal faces of $A'$.

theorem iso_bijective_fixing_chamber' {V : Type} [DecidableEq V] (b : Building V) (B : SimplicialComplex V) (hB : B ∈ b.apartmentSystem.apartments) (B₀ : SimplicialComplex V) (hB₀ : B₀ ∈ b.apartmentSystem.apartments) (D : Finset V) (hD_B : D ∈ B.faces) (hD_B₀ : D ∈ B₀.faces) (hD_max_B : B.IsMaximal D) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ B.faces ↔ Finset.image φ s ∈ B₀.faces) ∧ Finset.image φ D = D

For two apartments $B, B_0$ sharing a common chamber $D$, there is a bijective face-preserving isomorphism $B \to B_0$ that fixes $D$ setwise.

theorem bij_iso_fixing_chamber_is_id' {V : Type} [DecidableEq V] (b : Building V) (B B' : SimplicialComplex V) (hB : B ∈ b.apartmentSystem.apartments) (D : Finset V) (hD_B : D ∈ B.faces) (hD_max : b.IsMaximal D) (φ : V → V) (hφ_bij : Function.Bijective φ) (hφ_faces : ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image φ s ∈ B'.faces) (hφ_D : Finset.image φ D = D) (s : Finset V) : s ∈ B.faces → Finset.image φ s = s

By apartment-level unique labelling, any bijective face-preserving isomorphism $B \to B'$ that fixes a chamber $D$ setwise acts as the identity on every face of $B$.