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

A sector in a Euclidean apartment $A$ of a building: a base vertex together with a nonempty vertex set inside $A$, modeling a Weyl chamber (Section 16.5).

• apartment : SimplicialComplex V
• apartment_mem : self.apartment ∈ b.apartmentSystem.apartments
• baseVertex : V
• baseVertex_mem : ∃ s ∈ self.apartment.faces, self.baseVertex ∈ s
• vertices : Set V
• vertices_in_apartment (v : V) : v ∈ self.vertices → ∃ s ∈ self.apartment.faces, v ∈ s
• baseVertex_in_sector : self.baseVertex ∈ self.vertices
• nonempty : self.vertices.Nonempty

def AffineBuilding.Sector.SameDirection {V : Type} [DecidableEq V] (b : Building V) (S₁ S₂ : Sector b) : Prop

Two sectors $S_1, S_2$ point in the same direction iff they have subsectors $T_1 \subseteq S_1$ and $T_2 \subseteq S_2$ with $T_1.\text{vertices} = T_2.\text{vertices}$ — the parallelism relation underlying $X_\infty$ (Section 16.6).

def AffineBuilding.Sector.Direction {V : Type} [DecidableEq V] (b : Building V) : Type

A direction: the equivalence class of a sector under SameDirection, i.e. a point of $X_\infty$ at the sector level.

def AffineBuilding.Sector.Subsector {V : Type} [DecidableEq V] (b : Building V) (S' S : Sector b) : Prop

$S'$ is a subsector of $S$: $S'.\text{vertices} \subseteq S.\text{vertices}$ and the two sectors share a direction.

def AffineBuilding.Sector.IsOpposite {V : Type} [DecidableEq V] (b : Building V) (S₁ S₂ : Sector b) : Prop

$S_1$ and $S_2$ are opposite sectors: same apartment, and they contain subsectors sharing a common base vertex.

structure AffineBuilding.GeodesicRay {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Type

A geodesic ray in the affine building: a map $ℕ → V$ that is an isometric embedding for the building distance, $d(\rho(m), \rho(n)) = |m - n|$.

• toFun : ℕ → V
• isometry (m n : ℕ) : buildingDist b md (self.toFun m) (self.toFun n) = ↑(↑m - ↑n).natAbs

def AffineBuilding.GeodesicRay.Parallel {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (ρ₁ ρ₂ : GeodesicRay b md) : Prop

Two geodesic rays $\rho_1, \rho_2$ are parallel if $\sup_n d(\rho_1(n),\rho_2(n)) < \infty$ (bounded Hausdorff distance).

def AffineBuilding.PointAtInfinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Type

A point at infinity of the affine building: an equivalence class of geodesic rays under parallelism.

def AffineBuilding.Sector.pointsAtInfinity {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (md : ApartmentMetricData b) : Set (PointAtInfinity b md)

$S_\infty$: the set of points at infinity represented by geodesic rays that remain entirely inside the sector $S$.

def AffineBuilding.VertexInApartment {V : Type} [DecidableEq V] (A : SimplicialComplex V) (v : V) : Prop

Predicate: vertex $v$ belongs to some face of apartment $A$.

def AffineBuilding.SetInApartment {V : Type} [DecidableEq V] (A : SimplicialComplex V) (S : Set V) : Prop

Predicate: every vertex of $S$ lies in some face of apartment $A$.

theorem AffineBuilding.apt_face_extends_to_chamber_of_building {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ s ∈ A.faces, ∃ D ∈ A.faces, A.IsMaximal D ∧ s ⊆ D

Every face of an apartment extends to a maximal face (chamber) of that apartment.

structure AffineBuilding.SectorInfrastructure {V : Type} [DecidableEq V] (_b : Building V) : Prop

Auxiliary axiomatic data needed to manipulate sectors: every apartment face extends to a chamber, and the chamber containing a sector vertex is contained in the sector.

• apt_face_extends_to_chamber (A : SimplicialComplex V) : A ∈ _b.apartmentSystem.apartments → ∀ s ∈ A.faces, ∃ D ∈ A.faces, A.IsMaximal D ∧ s ⊆ D
• sector_chamber_closed (S : Sector _b) (D : Finset V) : D ∈ S.apartment.faces → S.apartment.IsMaximal D → (∃ v ∈ D, v ∈ S.vertices) → ∀ w ∈ D, w ∈ S.vertices

def AffineBuilding.SectorInfrastructure.mk' {V : Type} [DecidableEq V] (b : Building V) (sector_chamber_closed : ∀ (S : Sector b), ∀ D ∈ S.apartment.faces, S.apartment.IsMaximal D → (∃ v ∈ D, v ∈ S.vertices) → ∀ w ∈ D, w ∈ S.vertices) : SectorInfrastructure b

Convenience constructor for SectorInfrastructure using the building-level chamber extension lemma.

theorem AffineBuilding.SectorInfrastructure.sector_chamber_cover {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (S : Sector b) (v : V) : v ∈ S.vertices → ∃ D ∈ S.apartment.faces, S.apartment.IsMaximal D ∧ v ∈ D ∧ ∀ w ∈ D, w ∈ S.vertices

Every vertex of a sector lies in a chamber of the apartment contained entirely in the sector.

theorem AffineBuilding.SectorInfrastructure.sector_chambers_transfer {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (S : Sector b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hC : ∃ C ∈ A.faces, S.apartment.IsMaximal C ∧ ∀ v ∈ C, v ∈ S.vertices) (D : Finset V) (hD : D ∈ S.apartment.faces) (hD_max : S.apartment.IsMaximal D) (hD_in_S : ∀ w ∈ D, w ∈ S.vertices) : D ∈ A.faces

A chamber of a sector's apartment that is contained in the sector also belongs to any apartment $A$ sharing a chamber with the sector.

theorem AffineBuilding.SectorInfrastructure.sector_has_chamber {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (S : Sector b) : ∃ C ∈ S.apartment.faces, S.apartment.IsMaximal C ∧ ∀ v ∈ C, v ∈ S.vertices

Every sector contains at least one chamber (maximal face) of its apartment.

theorem AffineBuilding.SectorInfrastructure.sector_transfer {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (S : Sector b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hC : ∃ C ∈ A.faces, S.apartment.IsMaximal C ∧ ∀ v ∈ C, v ∈ S.vertices) : SetInApartment A S.vertices

If an apartment $A$ contains a chamber of a sector $S$, then $A$ contains every vertex of $S$.

theorem AffineBuilding.SectorInfrastructure.cone_vertex_subsector {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (S : Sector b) (v : V) (hv : v ∈ S.vertices) : ∃ (S' : Sector b), S'.apartment = S.apartment ∧ S'.baseVertex = v ∧ S'.vertices ⊆ S.vertices

For any vertex $v \in S$, the sector based at $v$ with the same vertex set is a subsector of $S$ with the same apartment.

theorem AffineBuilding.SectorInfrastructure.iso_from_shared_chamber {V : Type} [DecidableEq V] {b : Building V} (_si : SectorInfrastructure b) (A A' : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hA' : A' ∈ b.apartmentSystem.apartments) (C : Finset V) (hC_A : C ∈ A.faces) (hC_A' : C ∈ A'.faces) (hC_max : A.IsMaximal C) : ∃ (φ : SimplicialMap A A'), ∀ v ∈ C, φ.toFun v = v

Two apartments sharing a chamber $C$ admit an isomorphism that fixes $C$ pointwise.

theorem AffineBuilding.SectorInfrastructure.chamber_sector_common_apartment {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (C : Finset V) (hC : b.IsMaximal C) (S : Sector b) : ∃ A ∈ b.apartmentSystem.apartments, C ∈ A.faces ∧ ∃ (S' : Sector b), Sector.Subsector b S' S ∧ SetInApartment A S'.vertices

Given a chamber $C$ and a sector $S$, there exists an apartment $A$ containing $C$ and a subsector $S' \subseteq S$ (the key axiom of Section 16.7).

theorem AffineBuilding.SectorInfrastructure.sectors_any_common_apartment {V : Type} [DecidableEq V] {b : Building V} (si : SectorInfrastructure b) (S₁ S₂ : Sector b) : ∃ A ∈ b.apartmentSystem.apartments, SetInApartment A S₁.vertices ∧ SetInApartment A S₂.vertices

Any two sectors $S_1, S_2$ lie inside a common apartment of the building.

theorem AffineBuilding.Sector.SameDirection.refl {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) : SameDirection b S S

Reflexivity of SameDirection.

theorem AffineBuilding.Sector.SameDirection.symm {V : Type} [DecidableEq V] {b : Building V} {S₁ S₂ : Sector b} (h : SameDirection b S₁ S₂) : SameDirection b S₂ S₁

Symmetry of SameDirection.

theorem AffineBuilding.Sector.Subsector.refl {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) : Subsector b S S

Every sector is a subsector of itself.

theorem AffineBuilding.sectors_any_common_apartment' {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (S₁ S₂ : Sector b) : ∃ A ∈ b.apartmentSystem.apartments, SetInApartment A S₁.vertices ∧ SetInApartment A S₂.vertices

Convenience wrapper around SectorInfrastructure.sectors_any_common_apartment.