def closureSC {V : Type} [DecidableEq V] (C : Finset V) (hC : C.Nonempty) : SimplicialComplex V

The simplicial complex consisting of all non-empty subsets of a fixed chamber $C$ — the abstract closure of the simplex $C$.

structure LabellingRetraction {V : Type} [DecidableEq V] (b : Building V) : Type

A labelling-style retraction of a building $\mathcal{B}$ onto a chamber: data of a base chamber $C$, a vertex map $\rho$ sending each face to a face of $C$, injective on each face, and fixing $C$ pointwise.

• base : Finset V
• base_mem : self.base ∈ b.faces
• base_nonempty : self.base.Nonempty
• map : V → V
• map_face (s : Finset V) : s ∈ b.faces → Finset.image self.map s ⊆ self.base ∧ (Finset.image self.map s).Nonempty
• map_injOn_face (s : Finset V) : s ∈ b.faces → Set.InjOn self.map ↑s
• map_fixes_base (v : V) : v ∈ self.base → self.map v = v

structure DiscreteFibers.PointF {V : Type} [DecidableEq V] (Δ : SimplicialComplex V) : Type

A geometric point of the realisation $|\Delta|$ of a simplicial complex, given as a barycentric weight function $\mathrm{wt} : V \to \mathbb{R}_{\geq 0}$ supported on a single face $\sigma$ with weights summing to $1$.

• wt : V → ℝ
• face : Finset V
• face_mem : self.face ∈ Δ.faces
• wt_nonneg (v : V) : self.wt v ≥ 0
• wt_sum : ∑ v ∈ self.face, self.wt v = 1
• support_in_face (v : V) : self.wt v ≠ 0 → v ∈ self.face

def DiscreteFibers.star {V : Type} [DecidableEq V] {Δ : SimplicialComplex V} (x : PointF Δ) : Set (PointF Δ)

The open star of a point $x \in |\Delta|$: all points $z$ whose support lies, together with the support of $x$, inside a single common face.

noncomputable def DiscreteFibers.retractionMapWt {V : Type} [DecidableEq V] (ρ : V → V) (wt : V → ℝ) (σ : Finset V) : V → ℝ

The pushforward of a weight function $\mathrm{wt}$ supported on $\sigma$ along a vertex map $\rho$: the new weight at $v$ is $\sum_{u \in \sigma,\, \rho(u) = v} \mathrm{wt}(u)$.

noncomputable def DiscreteFibers.dist {V : Type} [DecidableEq V] {Δ : SimplicialComplex V} (p q : PointF Δ) : ℝ

The $L^\infty$ distance between two barycentric points: the supremum of $|p.\mathrm{wt}(v) - q.\mathrm{wt}(v)|$ over vertices in the union of their supports.

theorem labelling_retraction_injOn_building_face {V : Type} [DecidableEq V] (b : Building V) (ρ : LabellingRetraction b) (σ : Finset V) (hσ : σ ∈ b.faces) : Set.InjOn ρ.map ↑σ

A labelling retraction is injective on each building face.

theorem retraction_star_unique_preimage {V : Type} [DecidableEq V] (b : Building V) (ρ : LabellingRetraction b) (y : DiscreteFibers.PointF (closureSC ρ.base ⋯)) (x x' : DiscreteFibers.PointF b.toSimplicialComplex) (hx : ∀ (v : V), DiscreteFibers.retractionMapWt ρ.map x.wt x.face v = y.wt v) (hx' : ∀ (v : V), DiscreteFibers.retractionMapWt ρ.map x'.wt x'.face v = y.wt v) (hstar : x' ∈ DiscreteFibers.star x) : x.wt = x'.wt

Two points $x, x'$ that lie in the open star of one another and have the same image under a labelling retraction must coincide as weight functions — fibers are pointwise unique within a star.

theorem retraction_preimage_star_contains_ball {V : Type} [DecidableEq V] (b : Building V) (ρ : LabellingRetraction b) (y : DiscreteFibers.PointF (closureSC ρ.base ⋯)) : ∃ δ > 0, ∀ (x : DiscreteFibers.PointF b.toSimplicialComplex), (∀ (v : V), DiscreteFibers.retractionMapWt ρ.map x.wt x.face v = y.wt v) → ∀ (z : DiscreteFibers.PointF b.toSimplicialComplex), DiscreteFibers.dist x z < δ → z ∈ DiscreteFibers.star x

For any retraction image $y$ there is a uniform radius $\delta > 0$ such that every preimage point $x$ has its $\delta$-ball contained in its star — the fiber-with-star is a neighbourhood.

theorem retraction_preimage_discrete {V : Type} [DecidableEq V] (b : Building V) (ρ : LabellingRetraction b) (y : DiscreteFibers.PointF (closureSC ρ.base ⋯)) : ∃ δ > 0, ∀ (x x' : DiscreteFibers.PointF b.toSimplicialComplex), (∀ (v : V), DiscreteFibers.retractionMapWt ρ.map x.wt x.face v = y.wt v) → (∀ (v : V), DiscreteFibers.retractionMapWt ρ.map x'.wt x'.face v = y.wt v) → x.wt ≠ x'.wt → DiscreteFibers.dist x x' ≥ δ

The preimage of a point under a labelling retraction is discrete: two distinct preimages of $y$ are separated by at least a fixed positive distance $\delta$.