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

Strict inclusion is preserved by the image of an injective function on finite sets.

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

For any pair of chambers $C, D$ of an apartment $A$, there exists a bijective vertex map (apartment automorphism) sending $C$ to $D$.

theorem apt_bij_iso_label_preserving {V : Type} [DecidableEq V] (b : Building V) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (φ : V → V) (hφ_bij : Function.Bijective φ) (hφ_faces : ∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces) (L : Type) [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) (s : Finset V) (hs : s ∈ A.faces) : lab.labelMap (Finset.image φ s) = lab.labelMap s

A bijective vertex map between apartments that preserves the face structure is label-preserving.

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 face-preserving map between apartments sends maximal faces to maximal faces.

theorem apartment_iso_sending_chamber {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (B : SimplicialComplex V) (hB : B ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_max_bldg : b.IsMaximal C) (D : Finset V) (hD_B : D ∈ B.faces) (hD_max_bldg : b.IsMaximal D) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ B.faces ↔ Finset.image φ s ∈ A.faces) ∧ Finset.image φ D = C

For apartments $A, A'$ both containing a chamber $C$, there is an isomorphism $A \to A'$ that sends $C$ to itself (and is label-preserving).

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

A bijective apartment iso that fixes a chamber pointwise is the identity on the apartment.

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

Any apartment isomorphism fixing a chamber is automatically bijective.

theorem exists_canonical_retraction {V : Type} [DecidableEq V] (b : Building V) (B₀ : SimplicialComplex V) (hB₀ : B₀ ∈ b.apartmentSystem.apartments) (D : Finset V) (hD_B₀ : D ∈ B₀.faces) (hD_max : b.IsMaximal D) : ∃ (ρ : V → V), (∀ s ∈ b.faces, Finset.image ρ s ∈ B₀.faces) ∧ (∀ (v : V), (∃ s ∈ B₀.faces, v ∈ s) → ρ v = v) ∧ Finset.image ρ D = D ∧ (∀ B ∈ b.apartmentSystem.apartments, D ∈ B.faces → (Function.Injective fun (v : V) => ρ v) ∧ ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ρ s ∈ B₀.faces) ∧ ∀ s ∈ b.faces, Finset.image ρ s = s

Existence of the canonical retraction $\rho_{D;C,A} : X \to A$ centered at a chamber $C$ of an apartment $A$: a vertex-level retraction fixing $A$ pointwise and sending chambers to chambers.

theorem unique_retraction_D_to_C {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) (D : Finset V) (hD_max : b.IsMaximal D) : (∃ (ρ : V → V), (∀ s ∈ b.faces, Finset.image ρ s ∈ A.faces) ∧ (∀ (L : Type) [inst : DecidableEq L] (lab : Labelling b.toSimplicialComplex L), ∀ s ∈ b.faces, lab.labelMap (Finset.image ρ s) = lab.labelMap s) ∧ Finset.image ρ D = C ∧ ∀ B ∈ b.apartmentSystem.apartments, D ∈ B.faces → (Function.Injective fun (v : V) => ρ v) ∧ ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ρ s ∈ A.faces) ∧ ∀ (ρ₁ ρ₂ : V → V), (∀ s ∈ b.faces, Finset.image ρ₁ s ∈ A.faces) → (∀ (L : Type) [inst : DecidableEq L] (lab : Labelling b.toSimplicialComplex L), ∀ s ∈ b.faces, lab.labelMap (Finset.image ρ₁ s) = lab.labelMap s) → Finset.image ρ₁ D = C → (∀ B ∈ b.apartmentSystem.apartments, D ∈ B.faces → (Function.Injective fun (v : V) => ρ₁ v) ∧ ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ρ₁ s ∈ A.faces) → (∀ s ∈ b.faces, Finset.image ρ₂ s ∈ A.faces) → (∀ (L : Type) [inst : DecidableEq L] (lab : Labelling b.toSimplicialComplex L), ∀ s ∈ b.faces, lab.labelMap (Finset.image ρ₂ s) = lab.labelMap s) → Finset.image ρ₂ D = C → (∀ B ∈ b.apartmentSystem.apartments, D ∈ B.faces → (Function.Injective fun (v : V) => ρ₂ v) ∧ ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image ρ₂ s ∈ A.faces) → ∀ s ∈ b.faces, Finset.image ρ₁ s = Finset.image ρ₂ s

Uniqueness of the retraction $\rho_{D;C,A}$: any two retractions onto $A$ centered at $C$ with the same chamber-level behaviour agree (Section 15.5).