def Building.SimplicialComplexIso {V : Type u_1} [DecidableEq V] (A A' : SimplicialComplex V) : Prop

Two simplicial complexes on $V$ are isomorphic if there is a bijection $\varphi : V \to V$ that induces a bijection between their face sets.

def Building.ApartmentHasFoldings {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) : Prop

An apartment $A$ has foldings if its underlying simplicial complex extends to a chamber complex on which every pair of adjacent chambers admits a pair of foldings collapsing one chamber onto the other.

theorem Building.apartment_chamber_is_building_chamber {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hCmax : A.IsMaximal C) : b.IsMaximal C

A maximal simplex (chamber) of an apartment $A$ is also a maximal simplex of the ambient building.

theorem Building.building_chamber_in_apartment_is_apartment_chamber {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_in_A : C ∈ A.faces) (hCmax : b.IsMaximal C) : A.IsMaximal C

If a face $C$ of an apartment $A$ is maximal in the ambient building, then it is also maximal as a face of $A$.

theorem Building.apartment_has_chamber {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ C ∈ A.faces, A.IsMaximal C

Every apartment of a building contains a chamber (maximal face).

theorem Building.iso_exists_gives_iso {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hCA : C ∈ A.faces) (hCA' : C ∈ A'.faces) (hCmax : A.IsMaximal C) : SimplicialComplexIso A A'

Two apartments of a building that share a common chamber are isomorphic as simplicial complexes.

theorem Building.simplicialComplexIso_trans {V : Type u_1} [DecidableEq V] (A B A' : SimplicialComplex V) : SimplicialComplexIso A B → SimplicialComplexIso B A' → SimplicialComplexIso A A'

Simplicial complex isomorphism is transitive.

theorem Building.AllApartmentsIsomorphic {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ A' ∈ b.apartmentSystem.apartments, SimplicialComplexIso A A'

All apartments of a building are pairwise isomorphic as simplicial complexes. The proof uses that any two chambers lie in a common apartment and that apartments sharing a chamber are isomorphic.

structure Building.CoxeterTypeOfBuilding {V : Type u_1} [DecidableEq V] (b : Building V) : Type 1

The Coxeter type of a building: a Coxeter matrix $M$ together with the data, for each apartment $A$, of a labeling of its chambers by the Coxeter group $W(M)$ that is injective on chambers, surjective onto $W(M)$, and sends adjacent chambers to $W(M)$-adjacent group elements.

• B_idx : Type
• matrix : CoxeterMatrix self.B_idx
• apartments_iso (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∃ (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ ∃ (φ : Finset V → self.matrix.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) ∧ (∀ (w : self.matrix.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) ∧ ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent self.matrix (φ C) (φ C')

theorem Building.apartment_is_coxeter_complex {V : Type u_1} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ (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

Every apartment of a building is (canonically isomorphic to) a Coxeter complex: there exist a Coxeter matrix $M$ and a thin chamber complex structure whose chambers are in bijection with the Coxeter group $W(M)$ in an adjacency-preserving way.

theorem Building.finset_image_sdiff_of_inj {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s t : Finset α) (_hts : t ⊆ s) : Finset.image f (s \ t) = Finset.image f s \ Finset.image f t

For an injective $f$, the image of a set difference equals the difference of images: $f(s \setminus t) = f(s) \setminus f(t)$.

theorem Building.image_inv_image_eq {V : Type u_1} [DecidableEq V] {φ inv : V → V} (hright : ∀ (v : V), φ (inv v) = v) (s : Finset V) : Finset.image φ (Finset.image inv s) = s

If $\varphi \circ \mathrm{inv} = \mathrm{id}$ pointwise, then applying $\varphi$ to the $\mathrm{inv}$-image of $s$ recovers $s$.

theorem Building.image_phi_image_eq {V : Type u_1} [DecidableEq V] {φ inv : V → V} (hleft : ∀ (v : V), inv (φ v) = v) (s : Finset V) : Finset.image inv (Finset.image φ s) = s

If $\mathrm{inv} \circ \varphi = \mathrm{id}$ pointwise, then applying $\mathrm{inv}$ to the $\varphi$-image of $s$ recovers $s$.

theorem Building.iso_pullback_maximal {V : Type u_1} [DecidableEq V] {A₀ A : SimplicialComplex V} {φ inv : V → V} (hright : ∀ (v : V), φ (inv v) = v) (hleft : ∀ (v : V), inv (φ v) = v) (hφ_face : ∀ (s : Finset V), s ∈ A₀.faces ↔ Finset.image φ s ∈ A.faces) (C : Finset V) (hCmax : A.IsMaximal C) : A₀.IsMaximal (Finset.image inv C)

Under a simplicial complex isomorphism $\varphi : A_0 \to A$ with inverse $\mathrm{inv}$, the pullback by $\mathrm{inv}$ of a maximal face of $A$ is a maximal face of $A_0$.

theorem Building.iso_preserves_coxeter_type {V : Type u_1} [DecidableEq V] (b : Building V) (A₀ : SimplicialComplex V) (_hA₀ : A₀ ∈ b.apartmentSystem.apartments) (B_idx : Type) (M : CoxeterMatrix B_idx) (cc₀ : ChamberComplex V) (_hcc₀ : 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')) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hiso : SimplicialComplexIso A₀ A) : ∃ (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')

The Coxeter type of an apartment is preserved by simplicial isomorphism: if an apartment $A_0$ carries a labeling by a Coxeter group $W(M)$ realizing $A_0$ as the Coxeter complex of $M$, and $A_0 \cong A$, then $A$ also carries such a labeling for the same Coxeter matrix $M$.