structure AffineBuilding.IsSimplicialAutomorphism {V : Type} [DecidableEq V] (b : Building V) (f : V → V) : Prop

A simplicial automorphism of a building $\mathcal{B}$: a bijection on vertices that maps faces to faces and apartments to apartments.

• maps_faces (s : Finset V) : s ∈ b.faces → Finset.image f s ∈ b.faces
• bijective : Function.Bijective f
• maps_apartments (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∃ A' ∈ b.apartmentSystem.apartments, ∀ s ∈ A.faces, Finset.image f s ∈ A'.faces

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

An isometry of the building's vertex set with respect to the apartment metric: a vertex map $\varphi$ preserving the building distance.

• toFun : V → V
• isometry (v w : V) : buildingDist b md (self.toFun v) (self.toFun w) = buildingDist b md v w

noncomputable def AffineBuilding.BuildingIsometry.pushforwardRay {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : GeodesicRay b md) : GeodesicRay b md

The pushforward of a geodesic ray $\rho$ under a building isometry $\varphi$ is the composite ray $\varphi \circ \rho$.

theorem AffineBuilding.isometry_preserves_parallelism {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ₁ ρ₂ : GeodesicRay b md) (h : GeodesicRay.Parallel b md ρ₁ ρ₂) : GeodesicRay.Parallel b md (φ.pushforwardRay ρ₁) (φ.pushforwardRay ρ₂)

A building isometry preserves parallelism of geodesic rays: $\rho_1 \parallel \rho_2 \implies \varphi \rho_1 \parallel \varphi \rho_2$.

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

The origin $\rho(0)$ of a geodesic ray.

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

The point at infinity of a geodesic ray $\rho$, as the parallelism class of $\rho$.

theorem AffineBuilding.BuildingIsometry.pushforwardRay_origin {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : GeodesicRay b md) : (φ.pushforwardRay ρ).origin = φ.toFun ρ.origin

The origin of $\varphi \rho$ is $\varphi$ applied to the origin of $\rho$.

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

A geodesic ray parametrised by $\mathbb{R}_{\geq 0}$ rather than $\mathbb{N}$: a map $\rho : \mathbb{R}_{\geq 0} \to V$ that is an isometry onto its image.

• toFun : NNReal → V
• isometry (s t : NNReal) : buildingDist b md (self.toFun s) (self.toFun t) = |↑s - ↑t|

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

Two continuous geodesic rays are parallel iff they stay within a uniform distance $C \geq 0$ of each other at all times $t \geq 0$.

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

Points at infinity in the continuous parametrisation: parallelism classes of continuous geodesic rays.

noncomputable def AffineBuilding.BuildingIsometry.pushforwardContinuousRay {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : ContinuousGeodesicRay b md) : ContinuousGeodesicRay b md

Pushforward of a continuous geodesic ray under a building isometry.

theorem AffineBuilding.isometry_preserves_parallelism_continuous {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ₁ ρ₂ : ContinuousGeodesicRay b md) (h : ContinuousGeodesicRay.Parallel b md ρ₁ ρ₂) : ContinuousGeodesicRay.Parallel b md (φ.pushforwardContinuousRay ρ₁) (φ.pushforwardContinuousRay ρ₂)

A building isometry preserves parallelism of continuous geodesic rays.

noncomputable def AffineBuilding.BuildingIsometry.inducedMapInfinityCont {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) : ContinuousPointAtInfinity b md → ContinuousPointAtInfinity b md

The induced map $\varphi_\infty$ on continuous points at infinity: descended from the pushforward of rays through the parallelism quotient.

theorem AffineBuilding.BuildingIsometry.inducedMapInfinityCont_mk {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : ContinuousGeodesicRay b md) : φ.inducedMapInfinityCont (Quot.mk (ContinuousGeodesicRay.Parallel b md) ρ) = Quot.mk (ContinuousGeodesicRay.Parallel b md) (φ.pushforwardContinuousRay ρ)

The induced map $\varphi_\infty$ commutes with the parallelism quotient on continuous rays.

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

The origin $\rho(0)$ of a continuous geodesic ray.

def AffineBuilding.ContinuousGeodesicRay.pointAtInfinity {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (ρ : ContinuousGeodesicRay b md) : ContinuousPointAtInfinity b md

The point at infinity of a continuous geodesic ray.

theorem AffineBuilding.BuildingIsometry.pushforwardContinuousRay_origin {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : ContinuousGeodesicRay b md) : (φ.pushforwardContinuousRay ρ).origin = φ.toFun ρ.origin

The origin formula for the pushforward of a continuous ray.

theorem AffineBuilding.BuildingIsometry.pushforwardContinuousRay_pointAtInfinity {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : ContinuousGeodesicRay b md) : (φ.pushforwardContinuousRay ρ).pointAtInfinity = φ.inducedMapInfinityCont ρ.pointAtInfinity

The point-at-infinity formula for the pushforward of a continuous ray.

theorem AffineBuilding.isometry_ray_formula_cont {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : ContinuousGeodesicRay b md) : (φ.pushforwardContinuousRay ρ).origin = φ.toFun ρ.origin ∧ (φ.pushforwardContinuousRay ρ).pointAtInfinity = φ.inducedMapInfinityCont ρ.pointAtInfinity

Combined formula: pushing forward a continuous ray transports both its origin and its point at infinity.

noncomputable def AffineBuilding.BuildingIsometry.inducedMapInfinity {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) : PointAtInfinity b md → PointAtInfinity b md

The induced map $\varphi_\infty$ on points at infinity (discrete parametrisation) descending from ray pushforward.

theorem AffineBuilding.BuildingIsometry.inducedMapInfinity_mk {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : GeodesicRay b md) : φ.inducedMapInfinity (Quot.mk (GeodesicRay.Parallel b md) ρ) = Quot.mk (GeodesicRay.Parallel b md) (φ.pushforwardRay ρ)

The induced map $\varphi_\infty$ commutes with the parallelism quotient on rays.

theorem AffineBuilding.BuildingIsometry.pushforwardRay_pointAtInfinity {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) (ρ : GeodesicRay b md) : (φ.pushforwardRay ρ).pointAtInfinity = φ.inducedMapInfinity ρ.pointAtInfinity

Pushing forward a ray transports its point at infinity through $\varphi_\infty$.

theorem AffineBuilding.automorphism_maps_sectors_apartment {V : Type} [DecidableEq V] {b : Building V} (f : V → V) (hf : IsSimplicialAutomorphism b f) (S : Sector b) (A' : SimplicialComplex V) (hA' : A' ∈ b.apartmentSystem.apartments) (h_maps : ∀ s ∈ S.apartment.faces, Finset.image f s ∈ A'.faces) : ∃ (S' : Sector b), S'.vertices = f '' S.vertices ∧ S'.apartment = A'

If a simplicial automorphism $f$ sends a sector's apartment into an apartment $A'$, then the image $f(S)$ is again a sector with apartment $A'$.

theorem AffineBuilding.automorphism_maps_sectors {V : Type} [DecidableEq V] {b : Building V} (f : V → V) (hf : IsSimplicialAutomorphism b f) (S : Sector b) : ∃ (S' : Sector b), S'.vertices = f '' S.vertices

A simplicial automorphism sends every sector to another sector (in some apartment of the building's system).

theorem AffineBuilding.injective_face_map_maximal {V : Type} [DecidableEq V] {K : SimplicialComplex V} (h : V → V) (h_inj : Function.Injective h) (h_faces : ∀ s ∈ K.faces, Finset.image h s ∈ K.faces) (h_inv : V → V) (h_inv_faces : ∀ s ∈ K.faces, Finset.image h_inv s ∈ K.faces) (h_inv_left : ∀ (v : V), h_inv (h v) = v) (h_right : ∀ (v : V), h (h_inv v) = v) (C : Finset V) (hC : K.IsMaximal C) : K.IsMaximal (Finset.image h C)

An injective face-preserving map with a face-preserving two-sided inverse sends maximal faces to maximal faces.

theorem AffineBuilding.injective_face_map_adjacent {V : Type} [DecidableEq V] {K : SimplicialComplex V} (h : V → V) (h_inj : Function.Injective h) (h_faces : ∀ s ∈ K.faces, Finset.image h s ∈ K.faces) (h_inv : V → V) (h_inv_faces : ∀ s ∈ K.faces, Finset.image h_inv s ∈ K.faces) (h_inv_left : ∀ (v : V), h_inv (h v) = v) (h_right : ∀ (v : V), h (h_inv v) = v) (C D : Finset V) (hadj : K.Adjacent C D) : K.Adjacent (Finset.image h C) (Finset.image h D)

Such a bijective face-preserving map also preserves chamber adjacency.

theorem AffineBuilding.inverse_is_automorphism {V : Type} [DecidableEq V] {b : Building V} (f : V → V) (hf : IsSimplicialAutomorphism b f) : ∃ (g : V → V), IsSimplicialAutomorphism b g ∧ (∀ (v : V), g (f v) = v) ∧ ∀ (v : V), f (g v) = v

Every simplicial automorphism $f$ has a two-sided inverse $g$ which is also a simplicial automorphism.

theorem AffineBuilding.automorphism_is_isometry {V : Type} [DecidableEq V] {b : Building V} (md : ApartmentMetricData b) (f : V → V) (hf : IsSimplicialAutomorphism b f) (v w : V) : buildingDist b md (f v) (f w) = buildingDist b md v w

Every simplicial automorphism of a building is an isometry with respect to the apartment metric.

noncomputable def AffineBuilding.isometryOfAutomorphism {V : Type} [DecidableEq V] {b : Building V} (md : ApartmentMetricData b) (f : V → V) (hf : IsSimplicialAutomorphism b f) : BuildingIsometry b md

Package a simplicial automorphism as a BuildingIsometry.

theorem AffineBuilding.inducedSimplexMap_exists {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (σ : SimplexAtInfinity b md) : ∃ (τ : SimplexAtInfinity b md), τ.points = (isometryOfAutomorphism md f hf).inducedMapInfinity '' σ.points

Every automorphism induces a well-defined map on $X_\infty$: each simplex at infinity has an image simplex whose points are the $\varphi_\infty$ images of the original.

noncomputable def AffineBuilding.inducedSimplexMapOfAuto {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (σ : SimplexAtInfinity b md) : SimplexAtInfinity b md

The induced simplex map at infinity associated to a simplicial automorphism $f$.

theorem AffineBuilding.inducedSimplexMapOfAuto_points {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (σ : SimplexAtInfinity b md) : (inducedSimplexMapOfAuto f hf σ).points = (isometryOfAutomorphism md f hf).inducedMapInfinity '' σ.points

The points of $f_\infty(\sigma)$ are exactly $\varphi_\infty(\sigma.\mathrm{points})$.

theorem AffineBuilding.induced_automorphism_at_infinity {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) : ∃ (f_inf : PointAtInfinity b md → PointAtInfinity b md), (∀ (σ : SimplexAtInfinity b md), ∃ (τ : SimplexAtInfinity b md), τ.points = f_inf '' σ.points) ∧ (∀ (σ τ : SimplexAtInfinity b md), SimplexAtInfinity.IsFace b md σ τ → ∃ (σ' : SimplexAtInfinity b md) (τ' : SimplexAtInfinity b md), σ'.points = f_inf '' σ.points ∧ τ'.points = f_inf '' τ.points ∧ SimplexAtInfinity.IsFace b md σ' τ') ∧ ∀ (ρ : GeodesicRay b md), f_inf (Quot.mk (GeodesicRay.Parallel b md) ρ) = Quot.mk (GeodesicRay.Parallel b md) ((isometryOfAutomorphism md f hf).pushforwardRay ρ)

Every simplicial automorphism of a building induces an automorphism of $X_\infty$ that preserves simplices, face relations, and is compatible with ray pushforward.

theorem AffineBuilding.inducedSimplexMap_preserves_apartments {V : Type} [DecidableEq V] {b : Building V} {si : SectorInfrastructure b} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) : ∃ Ainf' ∈ allApartmentsAtInfinity b si md, ∀ σ ∈ Ainf.simplices, inducedSimplexMapOfAuto f hf σ ∈ Ainf'.simplices

The induced map sends apartments at infinity to apartments at infinity: each $A_\infty$ has an image $A_\infty'$ containing the images of all its simplices.

def AffineBuilding.BuildingIsometry.IsLabelPreserving {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} (φ : BuildingIsometry b md) {L : Type u_1} [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) : Prop

A building isometry preserves a chamber-complex labelling if the label of each face is invariant under $\varphi$.

def AffineBuilding.IsLabelPreservingAuto {V : Type} [DecidableEq V] (b : Building V) (f : V → V) {L : Type u_1} [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) : Prop

A simplicial automorphism preserves a labelling iff every face has the same label as its image.

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

A labelling of $X_\infty$: a label-finset map on simplices at infinity that is strictly monotone with respect to the face relation.

• labelMap : SimplexAtInfinity b md → Finset L_inf
• label_strictMono (σ τ : SimplexAtInfinity b md) : SimplexAtInfinity.IsFace b md σ τ → σ ≠ τ → self.labelMap σ ⊂ self.labelMap τ

theorem AffineBuilding.infinity_labelling_exists {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} {si : SectorInfrastructure b} : ∃ (L_inf : Type) (x : DecidableEq L_inf), Nonempty (InfinityLabelling L_inf)

$X_\infty$ admits a labelling: there exists a label type $L_\infty$ with a corresponding InfinityLabelling.

def AffineBuilding.InfinityLabelling.IsPreservedBy {V : Type} [DecidableEq V] {b : Building V} {md : ApartmentMetricData b} {L_inf : Type u_1} [DecidableEq L_inf] (lab : InfinityLabelling L_inf) (F : SimplexAtInfinity b md → SimplexAtInfinity b md) : Prop

A map $F$ on $X_\infty$ preserves a labelling iff each simplex has the same label as its image.

theorem AffineBuilding.induced_map_preserves_labels_on_apartment {V : Type} [DecidableEq V] {b : Building V} {si : SectorInfrastructure b} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) {L : Type u_1} [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) (hf_label : IsLabelPreservingAuto b f lab) {L_inf : Type u_2} [DecidableEq L_inf] (lab_inf : InfinityLabelling L_inf) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (σ : SimplexAtInfinity b md) (hσ : σ ∈ (apartmentBoundary b si md A hA).simplices) : lab_inf.labelMap (inducedSimplexMapOfAuto f hf σ) = lab_inf.labelMap σ

A label-preserving simplicial automorphism induces a label-preserving map on the simplices at infinity coming from any single apartment.

theorem AffineBuilding.stabilizer_maps_sectors_to_same_apartment {V : Type} [DecidableEq V] {b : Building V} (f : V → V) (hf : IsSimplicialAutomorphism b f) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_stab : ∀ s ∈ A.faces, Finset.image f s ∈ A.faces) (S : Sector b) (hS : S.apartment = A) : ∃ (S' : Sector b), S'.vertices = f '' S.vertices ∧ S'.apartment = A

If $f$ stabilises an apartment $A$ and $S$ is a sector in $A$, then $f(S)$ is again a sector inside $A$.

theorem AffineBuilding.stabilizes_implies_stabilizes_infinity {V : Type} [DecidableEq V] {b : Building V} {si : SectorInfrastructure b} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (h_stab : ∀ s ∈ A.faces, Finset.image f s ∈ A.faces) (Ainf : ApartmentAtInfinity b md) (hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (hAinf_from_A : Ainf.apartment = A) (σ : SimplexAtInfinity b md) : σ ∈ Ainf.simplices → inducedSimplexMapOfAuto f hf σ ∈ Ainf.simplices

Stabilising an apartment implies stabilising its apartment at infinity: the induced map sends $A_\infty$ to $A_\infty$ on the nose.

theorem AffineBuilding.stabilizer_infinity_implies_stabilizer {V : Type} [DecidableEq V] {b : Building V} {si : SectorInfrastructure b} {md : ApartmentMetricData b} (f : V → V) (hf : IsSimplicialAutomorphism b f) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (Ainf : ApartmentAtInfinity b md) (_hAinf : Ainf ∈ allApartmentsAtInfinity b si md) (_hAinf_from_A : Ainf.apartment = A) (_h_stab_inf : ∀ σ ∈ Ainf.simplices, inducedSimplexMapOfAuto f hf σ ∈ Ainf.simplices) (s : Finset V) : s ∈ A.faces → Finset.image f s ∈ A.faces

Converse: an automorphism that stabilises an apartment at infinity must stabilise the corresponding apartment $A$ in the building.