structure CombinatorialGeometry.ThreeChamberConfig {V : Type u_1} [DecidableEq V] (b : Building V) : Type u_1

Configuration of three chambers $C, D, E$ in a building, with apartments through each pair.

• C : Finset V
• D : Finset V
• E : Finset V
• hC : b.IsMaximal self.C
• hD : b.IsMaximal self.D
• hE : b.IsMaximal self.E
• apt_CD : SimplicialComplex V
• apt_CD_mem : self.apt_CD ∈ b.apartmentSystem.apartments
• hC_CD : self.C ∈ self.apt_CD.faces
• hD_CD : self.D ∈ self.apt_CD.faces
• apt_CE : SimplicialComplex V
• apt_CE_mem : self.apt_CE ∈ b.apartmentSystem.apartments
• hC_CE : self.C ∈ self.apt_CE.faces
• hE_CE : self.E ∈ self.apt_CE.faces
• apt_DE : SimplicialComplex V
• apt_DE_mem : self.apt_DE ∈ b.apartmentSystem.apartments
• hD_DE : self.D ∈ self.apt_DE.faces
• hE_DE : self.E ∈ self.apt_DE.faces

def CombinatorialGeometry.ThreeChamberConfig.TriangleInequality {V : Type u_1} [DecidableEq V] {b : Building V} (cfg : ThreeChamberConfig b) : Prop

Triangle inequality for gallery distance: $d(C, E) \le d(C, D) + d(D, E)$.

def CombinatorialGeometry.ThreeChamberConfig.IsCollinear {V : Type u_1} [DecidableEq V] {b : Building V} (cfg : ThreeChamberConfig b) : Prop

Three chambers $C, D, E$ are collinear if $d(C, E) = d(C, D) + d(D, E)$ (i.e. $D$ lies on a minimal gallery from $C$ to $E$).

def CombinatorialGeometry.StrongIsometry {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (S₁ S₂ : Set (Finset V)) (φ : Finset V → Finset V) : Prop

A strong isometry between subsets of chambers $S_1, S_2$ is a map preserving the Weyl-valued distance $\delta_W$.

def CombinatorialGeometry.SubsetInApartment {V : Type u_1} [DecidableEq V] (b : Building V) (S : Set (Finset V)) : Prop

$S$ lies in an apartment if there is some apartment $A$ of the building whose face set contains $S$.

theorem CombinatorialGeometry.StrongIsometryImpliesApartment {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) {Y : Set (Finset V)} {A : SimplicialComplex V} (hA : A ∈ b.apartmentSystem.apartments) {φ : Finset V → Finset V} (hφ : IsStrongIsometry δW Y (φ '' Y) φ) (hφ_img : ∀ C ∈ Y, φ C ∈ A.faces) : SubsetInApartment b Y

A strong $\delta_W$-isometry whose image lies in an apartment forces its domain to lie in an apartment as well.

theorem CombinatorialGeometry.identity_strong_isometry_of_subset {V : Type u_1} [DecidableEq V] {b : Building V} (δW : b.WValuedDist) (S : Set (Finset V)) (A : SimplicialComplex V) (_hA : A ∈ b.apartmentSystem.apartments) (hS : ∀ C ∈ S, C ∈ A.faces) (_hS_max : ∀ C ∈ S, b.IsMaximal C) : IsStrongIsometry δW S S id ∧ ∀ C ∈ S, id C ∈ A.faces

The identity map is a strong $\delta_W$-isometry from $S$ to itself.

structure CombinatorialGeometry.ThreeChamberHypotheses {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

Hypotheses underlying the three-chamber argument: concatenability of galleries and existence of a minimal gallery between any two maximal chambers.

• gallery_concat (C₁ C₂ C₃ : Finset V) (g₁ g₂ : Gallery b.toSimplicialComplex) : g₁.Connects C₁ C₂ → g₂.Connects C₂ C₃ → ∃ (g₃ : Gallery b.toSimplicialComplex), g₃.Connects C₁ C₃ ∧ g₃.length = g₁.length + g₂.length ∧ C₂ ∈ g₃.chambers
• minimal_gallery_exists (C D : Finset V) : b.IsMaximal C → b.IsMaximal D → ∃ (g : Gallery b.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist b.toSimplicialComplex C D

theorem CombinatorialGeometry.threeChamberHypotheses_of_building {V : Type u_1} [DecidableEq V] (b : Building V) : ThreeChamberHypotheses b

Every building canonically satisfies ThreeChamberHypotheses.

theorem CombinatorialGeometry.three_chambers_common_apartment {V : Type u_1} [DecidableEq V] (b : Building V) (hyp : ThreeChamberHypotheses b) (C₁ C₂ C₃ : Finset V) (hC₁ : b.IsMaximal C₁) (hC₂ : b.IsMaximal C₂) (hC₃ : b.IsMaximal C₃) (hcollinear : galleryDist b.toSimplicialComplex C₁ C₃ = galleryDist b.toSimplicialComplex C₁ C₂ + galleryDist b.toSimplicialComplex C₂ C₃) : ∃ A ∈ b.apartmentSystem.apartments, C₁ ∈ A.faces ∧ C₂ ∈ A.faces ∧ C₃ ∈ A.faces

Three-chambers-in-a-common-apartment: if $C_1, C_2, C_3$ are collinear chambers (i.e. $d(C_1, C_3) = d(C_1, C_2) + d(C_2, C_3)$), then they all lie in some common apartment.