def AffineBuilding.SimplexAtInfinity.IsFace {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (σ τ : SimplexAtInfinity b md) : Prop

$\sigma$ is a face of $\tau$ in $X_\infty$ iff $\sigma.\text{points} \subseteq \tau.\text{points}$.

theorem AffineBuilding.SimplexAtInfinity.IsFace.refl {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (σ : SimplexAtInfinity b md) : IsFace b md σ σ

Reflexivity of the face relation on simplices at infinity.

theorem AffineBuilding.SimplexAtInfinity.IsFace.trans {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} {σ τ ρ : SimplexAtInfinity b md} (h₁ : IsFace b md σ τ) (h₂ : IsFace b md τ ρ) : IsFace b md σ ρ

Transitivity of the face relation.

theorem AffineBuilding.SimplexAtInfinity.IsFace.antisymm_points {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} {σ τ : SimplexAtInfinity b md} (h₁ : IsFace b md σ τ) (h₂ : IsFace b md τ σ) : σ.points = τ.points

Antisymmetry of the face relation at the point-set level.

theorem AffineBuilding.SimplexAtInfinity.ext' {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} {σ τ : SimplexAtInfinity b md} (h : σ.points = τ.points) : σ = τ

Extensionality: simplices at infinity are equal iff their point sets coincide.

def AffineBuilding.FacePoset {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (S : Set (SimplexAtInfinity b md)) (σ : SimplexAtInfinity b md) : Type

The face poset below $\sigma$ inside a chosen set $S$ of simplices at infinity.

@[implicit_reducible]

instance AffineBuilding.FacePoset.instPartialOrder {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (S : Set (SimplexAtInfinity b md)) (σ : SimplexAtInfinity b md) : PartialOrder (FacePoset b md S σ)

Partial order on FacePoset induced by the face relation on simplices at infinity.

noncomputable def AffineBuilding.apartmentBoundary {V : Type} [DecidableEq V] (b : Building V) (_si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ApartmentAtInfinity b md

$A_\infty$: the apartment at infinity built from a Euclidean apartment $A$, consisting of all ideal simplices arising from sectors in $A$.

def AffineBuilding.allSimplicesAtInfinity {V : Type} [DecidableEq V] (b : Building V) (_si : SectorInfrastructure b) (md : ApartmentMetricData b) : Set (SimplexAtInfinity b md)

The full set of ideal simplices: simplices contained in $S_\infty$ for some sector $S$ of some apartment of $X$.

def AffineBuilding.allApartmentsAtInfinity {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : Set (ApartmentAtInfinity b md)

The set of apartments-at-infinity, one for each Euclidean apartment via apartmentBoundary.

theorem AffineBuilding.apartment_simplices_sub {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) : Ainf.simplices ⊆ allSimplicesAtInfinity b si md ∧ ∀ (σ τ : SimplexAtInfinity b md), σ ∈ Ainf.simplices → SimplexAtInfinity.IsFace b md τ σ → τ ∈ Ainf.simplices

Every apartment-at-infinity injects into the global simplex set and is closed under taking faces.

structure AffineBuilding.BuildingAtInfinity.IsSimplicialSubcomplex {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (Binf : BuildingAtInfinity b md) (sub : Set (SimplexAtInfinity b md)) : Prop

A subset of simplices at infinity is a simplicial subcomplex of $X_\infty$: it is contained in the building's simplex set and closed under taking faces.

• subset : sub ⊆ Binf.simplices
• face_closed (σ τ : SimplexAtInfinity b md) : σ ∈ sub → SimplexAtInfinity.IsFace b md τ σ → τ ∈ sub

theorem AffineBuilding.any_two_simplices_common_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (σ₁ : SimplexAtInfinity b md) (hσ₁ : σ₁ ∈ allSimplicesAtInfinity b si md) (σ₂ : SimplexAtInfinity b md) (hσ₂ : σ₂ ∈ allSimplicesAtInfinity b si md) : ∃ Ainf ∈ allApartmentsAtInfinity b si md, σ₁ ∈ Ainf.simplices ∧ σ₂ ∈ Ainf.simplices

Any two ideal simplices lie in a common apartment-at-infinity — the building axiom (BU1) for $X_\infty$ (Section 16.9).

noncomputable def AffineBuilding.buildBoundaryComplex {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : BuildingAtInfinity b md

Constructs the building at infinity $X_\infty$ as a BuildingAtInfinity, using all ideal simplices and all apartment boundaries.

theorem AffineBuilding.sector_pointsAtInfinity_bounded {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (S : Sector b) : ∃ (n : ℕ) (f : ↑(S.pointsAtInfinity md) → Fin n), Function.Injective f

The set $S_\infty$ of points at infinity of a sector $S$ embeds injectively into some Fin n, hence is finite.

theorem AffineBuilding.sector_finite_points_at_infinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (S : Sector b) : (S.pointsAtInfinity md).Finite

$S_\infty$ is finite as a set of points at infinity.

theorem AffineBuilding.subsector_pointsAtInfinity_eq {V : Type} [DecidableEq V] {b : Building V} (md : ApartmentMetricData b) (T S : Sector b) (h : T.vertices ⊆ S.vertices) : T.pointsAtInfinity md = S.pointsAtInfinity md

A subsector $T \subseteq S$ has the same set of points at infinity as $S$.

theorem AffineBuilding.pointsAtInfinity_eq_of_vertices_eq {V : Type} [DecidableEq V] {b : Building V} (md : ApartmentMetricData b) (S₁ S₂ : Sector b) (hv : S₁.vertices = S₂.vertices) : S₁.pointsAtInfinity md = S₂.pointsAtInfinity md

Sectors with identical vertex sets have identical points at infinity.

theorem AffineBuilding.same_direction_same_pointsAtInfinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (S₁ S₂ : Sector b) (h : Sector.SameDirection b S₁ S₂) : S₁.pointsAtInfinity md = S₂.pointsAtInfinity md

Sectors with the same direction have the same set of points at infinity.

theorem AffineBuilding.apartment_sector_directions_finite {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : {d : Sector.Direction b | ∃ (S : Sector b), S.apartment = A ∧ d = Quot.mk (Sector.SameDirection b) S}.Finite

The set of sector directions arising from sectors of a fixed apartment is finite.

theorem AffineBuilding.sector_direction_classification {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ (n : ℕ), Nonempty (↑{d : Sector.Direction b | ∃ (S : Sector b), S.apartment = A ∧ d = Quot.mk (Sector.SameDirection b) S} ≃ Fin n)

The set of sector directions in an apartment is in bijection with some Fin n.

theorem AffineBuilding.apartment_finitely_many_sector_directions {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : {d : Sector.Direction b | ∃ (S : Sector b), S.apartment = A ∧ d = Quot.mk (Sector.SameDirection b) S}.Finite

An apartment has finitely many sector directions.

theorem AffineBuilding.apartment_finitely_many_sector_point_sets {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : {T : Set (PointAtInfinity b md) | ∃ (S : Sector b), S.apartment = A ∧ T = S.pointsAtInfinity md}.Finite

The collection of distinct point-sets $S_\infty$ over sectors of an apartment is finite.

theorem AffineBuilding.apartment_finite_points_at_infinity {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : {p : PointAtInfinity b md | ∃ (S : Sector b), S.apartment = A ∧ p ∈ S.pointsAtInfinity md}.Finite

The set of points at infinity lying in some sector of a fixed apartment is finite.

theorem AffineBuilding.coxeter_complex_finite_simplices_for_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : (apartmentBoundary b si md A hA).simplices.Finite

An apartment-at-infinity has finitely many simplices (the Coxeter-complex finiteness needed for sphericality).

theorem AffineBuilding.apartment_boundary_finite {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) : Ainf.simplices.Finite

Each apartment-at-infinity has finitely many simplices.

theorem AffineBuilding.buildBoundaryComplex_isSpherical {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (h_nonempty : b.apartmentSystem.apartments.Nonempty) : BuildingAtInfinity.IsSpherical b md (buildBoundaryComplex b si md)

The building at infinity $X_\infty$ is spherical — combines apartment finiteness with nonemptiness (Section 16.10).

theorem AffineBuilding.exists_spherical_building_at_infinity {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (h_nonempty : b.apartmentSystem.apartments.Nonempty) : ∃ (Binf : BuildingAtInfinity b md), BuildingAtInfinity.IsSpherical b md Binf

Existence form of the previous theorem: a spherical $X_\infty$ exists.

def AffineBuilding.ApartmentBoundary_face_lattice_is_powerset {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : Prop

The face lattice below a simplex in an apartment-at-infinity is order-isomorphic to a finite powerset $\mathcal{P}(\text{Fin}\,n)$ — the "simplicial complex" axiom.

theorem AffineBuilding.apartmentBoundary_coxeter_face_completeness {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (σ : SimplexAtInfinity b md) (hσ : σ ∈ (apartmentBoundary b si md A hA).simplices) (T : Set (PointAtInfinity b md)) (hT_ne : T.Nonempty) (hT_sub : T ⊆ σ.points) : ∃ τ ∈ (apartmentBoundary b si md A hA).simplices, τ.points = T

Face completeness: every nonempty subset $T$ of the points of a simplex in $A_\infty$ is itself realized as the point set of some simplex in $A_\infty$.

theorem AffineBuilding.simplex_points_finite_in_boundary {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (σ : SimplexAtInfinity b md) (hσ : σ ∈ (apartmentBoundary b si md A hA).simplices) : σ.points.Finite

Every simplex in an apartment-at-infinity has a finite point set.

noncomputable def AffineBuilding.withBotNonemptyEquivFinset (n : ℕ) : WithBot { s : Finset (Fin n) // s.Nonempty } ≃o Finset (Fin n)

Order isomorphism between $\text{WithBot}\{s : \text{Finset}(\text{Fin}\,n) // s.\text{Nonempty}\}$ and $\text{Finset}(\text{Fin}\,n)$, sending $\bot$ to $\emptyset$.

theorem AffineBuilding.coxeter_complex_powerset_for_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (σ : SimplexAtInfinity b md) (hσ : σ ∈ (apartmentBoundary b si md A hA).simplices) : ∃ (n : ℕ), Nonempty (WithBot (FacePoset b md (apartmentBoundary b si md A hA).simplices σ) ≃o Finset (Fin n))

The face poset below $\sigma$ in $A_\infty$ is order-isomorphic to a finite powerset.

theorem AffineBuilding.apartmentBoundary_face_lattice_is_powerset {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : ApartmentBoundary_face_lattice_is_powerset b si md

Globalized version of coxeter_complex_powerset_for_apartment packaged via ApartmentBoundary_face_lattice_is_powerset.

def AffineBuilding.ApartmentBoundary_glb_in_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : Prop

Predicate: every pair of simplices in any apartment-at-infinity has a greatest common subface — the "meet exists" axiom.

theorem AffineBuilding.minimum_face_in_apartment {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ (σ_min : SimplexAtInfinity b md), ∀ (S : Sector b), S.apartment = A → σ_min.points ⊆ S.pointsAtInfinity md ∧ ∀ (σ : SimplexAtInfinity b md), σ.points ⊆ S.pointsAtInfinity md → σ_min.points ⊆ σ.points

Every apartment-at-infinity has a minimum simplex contained in every $S_\infty$.

theorem AffineBuilding.spherical_coxeter_minimum_element {V : Type} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ (p : PointAtInfinity b md), ∀ (S : Sector b) (σ : SimplexAtInfinity b md), S.apartment = A → σ.points ⊆ S.pointsAtInfinity md → p ∈ σ.points

A point-level minimum: some point at infinity belongs to every $S_\infty$ of $A$.

theorem AffineBuilding.apartmentBoundary_has_minimum_vertex {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) : ∃ (p : PointAtInfinity b md), ∀ σ ∈ (apartmentBoundary b si md A hA).simplices, p ∈ σ.points

Every simplex of $A_\infty$ contains a common minimum vertex point at infinity.

theorem AffineBuilding.coxeter_complex_common_point_for_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (σ₁ σ₂ : SimplexAtInfinity b md) (hσ₁ : σ₁ ∈ (apartmentBoundary b si md A hA).simplices) (hσ₂ : σ₂ ∈ (apartmentBoundary b si md A hA).simplices) : (σ₁.points ∩ σ₂.points).Nonempty

Any two simplices of $A_\infty$ share at least one common point at infinity.

theorem AffineBuilding.apartment_boundary_simplices_share_point {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (σ₁ σ₂ : SimplexAtInfinity b md) (hσ₁ : σ₁ ∈ Ainf.simplices) (hσ₂ : σ₂ ∈ Ainf.simplices) : (σ₁.points ∩ σ₂.points).Nonempty

Apartment-level corollary: any two simplices of a generic apartment-at-infinity share a common point.

theorem AffineBuilding.apartment_boundary_maximal_face_in_set {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (T : Set (PointAtInfinity b md)) (hT_ne : T.Nonempty) (hT_from_sector : ∃ (S : Sector b), S.apartment = Ainf.apartment ∧ T ⊆ S.pointsAtInfinity md) (σ : SimplexAtInfinity b md) (hσ : σ ∈ Ainf.simplices) (hσT : σ.points ⊆ T) : ∃ γ ∈ Ainf.simplices, γ.points ⊆ T ∧ ∀ δ ∈ Ainf.simplices, δ.points ⊆ T → δ.points ⊆ γ.points

Among all simplices of $A_\infty$ contained in a given point set $T$, there is a maximal one (containing every other such simplex).

theorem AffineBuilding.apartmentBoundary_glb_in_apartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : ApartmentBoundary_glb_in_apartment b si md

Apartments-at-infinity admit greatest lower bounds for pairs of simplices.

structure AffineBuilding.BuildingAtInfinity.IsSimplicialComplex {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (Binf : BuildingAtInfinity b md) : Prop

$X_\infty$ is a simplicial complex: each simplex's face lattice is a powerset and every pair of simplices has a glb (Section 16.9).

• face_lattice_powerset (σ : SimplexAtInfinity b md) : σ ∈ Binf.simplices → ∃ (n : ℕ), Nonempty (WithBot (FacePoset b md Binf.simplices σ) ≃o Finset (Fin n))
• glb_exists (σ₁ σ₂ : SimplexAtInfinity b md) : σ₁ ∈ Binf.simplices → σ₂ ∈ Binf.simplices → ∃ γ ∈ Binf.simplices, SimplexAtInfinity.IsFace b md γ σ₁ ∧ SimplexAtInfinity.IsFace b md γ σ₂ ∧ ∀ δ ∈ Binf.simplices, SimplexAtInfinity.IsFace b md δ σ₁ → SimplexAtInfinity.IsFace b md δ σ₂ → SimplexAtInfinity.IsFace b md δ γ

theorem AffineBuilding.face_in_apartment_boundary {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (σ τ : SimplexAtInfinity b md) (hσ : σ ∈ Ainf.simplices) (hface : SimplexAtInfinity.IsFace b md τ σ) : τ ∈ Ainf.simplices

A face of a simplex of $A_\infty$ is itself a simplex of $A_\infty$.

theorem AffineBuilding.apartment_is_subcomplex {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) : (buildBoundaryComplex b si md).IsSimplicialSubcomplex Ainf.simplices

Each apartment-at-infinity is a simplicial subcomplex of $X_\infty$.

noncomputable def AffineBuilding.facePosetIsoOfApartment {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (σ : SimplexAtInfinity b md) (hσ : σ ∈ Ainf.simplices) : FacePoset b md (allSimplicesAtInfinity b si md) σ ≃o FacePoset b md Ainf.simplices σ

Order isomorphism: the face poset of $\sigma$ in $X_\infty$ agrees with the face poset in any apartment $A_\infty$ containing $\sigma$.

theorem AffineBuilding.buildBoundaryComplex_SC1 {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (σ : SimplexAtInfinity b md) (hσ : σ ∈ allSimplicesAtInfinity b si md) : ∃ (n : ℕ), Nonempty (WithBot (FacePoset b md (allSimplicesAtInfinity b si md) σ) ≃o Finset (Fin n))

Axiom SC1 for $X_\infty$: the face lattice below every simplex is a powerset.

theorem AffineBuilding.buildBoundaryComplex_SC2 {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (σ₁ σ₂ : SimplexAtInfinity b md) (hσ₁ : σ₁ ∈ allSimplicesAtInfinity b si md) (hσ₂ : σ₂ ∈ allSimplicesAtInfinity b si md) : ∃ γ ∈ allSimplicesAtInfinity b si md, SimplexAtInfinity.IsFace b md γ σ₁ ∧ SimplexAtInfinity.IsFace b md γ σ₂ ∧ ∀ δ ∈ allSimplicesAtInfinity b si md, SimplexAtInfinity.IsFace b md δ σ₁ → SimplexAtInfinity.IsFace b md δ σ₂ → SimplexAtInfinity.IsFace b md δ γ

Axiom SC2 for $X_\infty$: every pair of simplices has a greatest lower bound.

theorem AffineBuilding.buildBoundaryComplex_isSimplicialComplex {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) : (buildBoundaryComplex b si md).IsSimplicialComplex

$X_\infty$ is a simplicial complex — combines SC1 and SC2.

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

A spherical simplicial complex at infinity: bundles BuildingAtInfinity with proofs that it is spherical and a simplicial complex.

• building : BuildingAtInfinity b md
• spherical : BuildingAtInfinity.IsSpherical b md self.building
• simplicialComplex : self.building.IsSimplicialComplex

noncomputable def AffineBuilding.buildBoundarySimplicialComplex {V : Type} [DecidableEq V] (b : Building V) (si : SectorInfrastructure b) (md : ApartmentMetricData b) (h_nonempty : b.apartmentSystem.apartments.Nonempty) : SphericalSimplicialComplex b md

Bundled constructor: produces a SphericalSimplicialComplex from $X$, $si$, and $md$.