def IsTypePreservingIso {V : Type} [DecidableEq V] {L : Type u_1} [DecidableEq L] {b : Building V} (A A' : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) (_hA' : A' ∈ b.apartmentSystem.apartments) (lab : Labelling b.toSimplicialComplex L) (f : SimplicialMap A A') : Prop

A simplicial map $f : A \to A'$ between two apartments of a building is type- (or label-) preserving if applying $f$ to any face leaves its labelling unchanged.

def ApartmentSystem.le {V : Type} [DecidableEq V] {K : ChamberComplex V} (𝒜₁ 𝒜₂ : ApartmentSystem K) : Prop

Order on apartment systems: $\mathcal A_1 \le \mathcal A_2$ if every apartment of $\mathcal A_1$ also belongs to $\mathcal A_2$.

theorem bij_iso_fixing_chamber_is_id_gen {V : Type} [DecidableEq V] (b : Building V) (𝒜 : ApartmentSystem b.toChamberComplex) (B B' : SimplicialComplex V) (hB : B ∈ 𝒜.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 vertex map of an apartment that fixes some chamber pointwise is the identity on every face of the apartment.

theorem apt_automorphism_sending_chamber_gen {V : Type} [DecidableEq V] (b : Building V) (𝒜 : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜.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

Chamber-transitive automorphism: for any pair of chambers $C, D$ of an apartment $A$, there is a bijective vertex map sending $C$ to $D$.

theorem apt_faces_subset_gen {V : Type} [DecidableEq V] (b : Building V) (𝒜 : ApartmentSystem b.toChamberComplex) (A B : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (hB : B ∈ 𝒜.apartments) (C : Finset V) (hCA : C ∈ A.faces) (hCB : C ∈ B.faces) (hCmax : b.IsMaximal C) : B.faces ⊆ A.faces

An apartment's faces are determined by its chambers: if all chambers of $A$ lie in $A'$, then so do all faces.

theorem building_faces_subset_apt_gen {V : Type} [DecidableEq V] (b : Building V) (𝒜 : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (C : Finset V) (hCA : C ∈ A.faces) (hCmax : b.IsMaximal C) (s : Finset V) : s ∈ b.faces → s ∈ A.faces

If an apartment contains every chamber of the building, it contains every face of the building.

theorem cross_system_retraction_pair {V : Type} [DecidableEq V] (b : Building V) (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) : ∃ (ρ : V → V) (σ : V → V), (∀ s ∈ A.faces, Finset.image ρ s ∈ A'.faces) ∧ (∀ s ∈ A'.faces, Finset.image σ s ∈ A.faces) ∧ (∀ (v : V), σ (ρ v) = v) ∧ (∀ (v : V), ρ (σ v) = v) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → ρ v = v) ∧ ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → σ v = v

For two apartment systems with a common apartment $A$ and chamber $C$, the canonical retractions onto $A$ from each system agree on $A$.

theorem cross_system_iso_exists {V : Type} [DecidableEq V] (b : Building V) (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) : ∃ (φ : SimplicialMap A A'), Function.Bijective φ.toFun ∧ (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ.toFun s ∈ A'.faces) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) ∧ ∀ v ∈ C, φ.toFun v = v

Between any two apartments sharing a chamber, there exists an isomorphism $A \to A'$ fixing $A \cap A'$ pointwise.

theorem cross_system_iso_bijective {V : Type} [DecidableEq V] (b : Building V) (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (_hCA : C ∈ A.faces) (hCA' : C ∈ A'.faces) (hCmax : A.IsMaximal C) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces) ∧ ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ v = v

The cross-system isomorphism $A \to A'$ is bijective on vertices.

theorem cross_system_iso_preserves_labels {V : Type} [DecidableEq V] (b : Building V) {L : Type} [DecidableEq L] (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) (lab : Labelling b.toSimplicialComplex L) : ∃ (φ : SimplicialMap A A'), (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) ∧ ∀ s ∈ A.faces, lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s

The cross-system isomorphism $A \to A'$ is label-preserving.

theorem any_iso_fixing_intersection_preserves_labels {V : Type} [DecidableEq V] (b : Building V) {L : Type} [DecidableEq L] (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) (lab : Labelling b.toSimplicialComplex L) (φ : SimplicialMap A A') (hφ_bij : Function.Bijective φ.toFun) (hφ_fix : ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) (s : Finset V) : s ∈ A.faces → lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s

Any chamber-complex isomorphism $A \to A'$ that fixes $A \cap A'$ pointwise is automatically label-preserving (Section 4.4 corollary).

theorem section_4_4_corollary {V : Type} [DecidableEq V] (b : Building V) {L : Type} [DecidableEq L] (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) (lab : Labelling b.toSimplicialComplex L) : (∃ (φ : SimplicialMap A A'), (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) ∧ ∀ s ∈ A.faces, lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s) ∧ ∀ (φ : SimplicialMap A A'), Function.Bijective φ.toFun → (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) → ∀ s ∈ A.faces, lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s

Section 4.4 corollary: for apartments $A, A'$ in a given apartment system with a chamber in common, there is a label-preserving chamber-complex isomorphism $f : A \to A'$ fixing $A \cap A'$ pointwise, and any isomorphism fixing $A \cap A'$ pointwise is label-preserving.

theorem cross_system_iso_exists_for_apt_system {V : Type} [DecidableEq V] (b : Building V) (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (x : Finset V) (hxA : x ∈ A.faces) (hxA' : x ∈ A'.faces) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) : ∃ (φ : SimplicialMap A A'), (∀ v ∈ x, φ.toFun v = v) ∧ ∀ v ∈ C, φ.toFun v = v

Specialisation of cross-system isomorphism existence to the given apartment system.

theorem cross_system_iso_bijective_for_apt_system {V : Type} [DecidableEq V] (b : Building V) (𝒜₁ 𝒜₂ : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜₁.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜₂.apartments) (C : Finset V) (_hCA : C ∈ A.faces) (hCA' : C ∈ A'.faces) (hCmax : A.IsMaximal C) : ∃ (φ : V → V), Function.Bijective φ ∧ ∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces

The cross-system isomorphism is bijective for any two apartments in the same apartment system sharing a chamber.

theorem apartment_union_is_apartment_system {V : Type} [DecidableEq V] (b : Building V) : ∃ (𝒜_max : ApartmentSystem b.toChamberComplex), 𝒜_max.apartments = ⋃ (𝒜 : ApartmentSystem b.toChamberComplex), 𝒜.apartments

The union of all apartment systems of a building is itself an apartment system (the maximal apartment system, Section 15.5).

theorem apartment_system_subset_union {V : Type} [DecidableEq V] (b : Building V) (𝒜_max : ApartmentSystem b.toChamberComplex) (h_max : 𝒜_max.apartments = ⋃ (𝒜 : ApartmentSystem b.toChamberComplex), 𝒜.apartments) (𝒜' : ApartmentSystem b.toChamberComplex) : 𝒜'.apartments ⊆ 𝒜_max.apartments

Every apartment system is contained in the union of all apartment systems.

theorem apartment_system_maximal_unique {V : Type} [DecidableEq V] (b : Building V) (𝒜_max : ApartmentSystem b.toChamberComplex) (h_max : 𝒜_max.apartments = ⋃ (𝒜 : ApartmentSystem b.toChamberComplex), 𝒜.apartments) (𝒜' : ApartmentSystem b.toChamberComplex) (h_all : ∀ (𝒜'' : ApartmentSystem b.toChamberComplex), 𝒜''.apartments ⊆ 𝒜'.apartments) : 𝒜_max.apartments = 𝒜'.apartments

The maximal apartment system is unique: any apartment system that contains the union must equal it.

structure Building.MaximalApartmentSystem {V : Type} [DecidableEq V] (b : Building V) : Type

The bundled maximal apartment system of a building, together with the fact that it contains every apartment system.

• system : ApartmentSystem b.toChamberComplex
• contains_all (𝒜' : ApartmentSystem b.toChamberComplex) : 𝒜'.apartments ⊆ self.system.apartments
• unique (𝒜' : ApartmentSystem b.toChamberComplex) : (∀ (𝒜'' : ApartmentSystem b.toChamberComplex), 𝒜''.apartments ⊆ 𝒜'.apartments) → self.system.apartments = 𝒜'.apartments

noncomputable def SimplicialComplex.linkDiameter {V : Type} [DecidableEq V] (K : SimplicialComplex V) (F : Finset V) (hF : F ∈ K.faces) : ℕ

The diameter of the link of a simplex $x$ inside the complex $K$.

def Building.CoxeterDataFromLinks {V : Type} [DecidableEq V] {B : Type u_1} [DecidableEq B] [Fintype B] (b : Building V) (M : CoxeterMatrix B) (lab : Labelling b.toSimplicialComplex B) (C : Finset V) (_hC : b.IsMaximal C) : Prop

The Coxeter data attached to a building, extracted from the diameters of its links.