structure GeometricRealization.Point {V : Type u_1} [DecidableEq V] [Fintype V] (Δ : SimplicialComplex V) : Type u_1

A point of the geometric realization $|\Delta|$ of a simplicial complex $\Delta$: a barycentric weighting of vertices that sums to $1$ and whose support lies in some face of $\Delta$.

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

noncomputable def GeometricRealization.dist {V : Type u_1} [DecidableEq V] [Fintype V] [Nonempty V] {Δ : SimplicialComplex V} (p q : Point Δ) : ℝ

$\ell^\infty$ distance between two points in $|\Delta|$: the supremum of $|p_v - q_v|$ over $v$.

noncomputable def GeometricRealization.vertexEmbedding {V : Type u_1} [DecidableEq V] [Fintype V] (Δ : SimplicialComplex V) (v : V) (hv : {v} ∈ Δ.faces) : Point Δ

The canonical embedding of a vertex $v$ as the corresponding $\delta_v$-point of $|\Delta|$.

noncomputable def GeometricRealization.support {V : Type u_1} [DecidableEq V] [Fintype V] {Δ : SimplicialComplex V} (p : Point Δ) : Finset V

The support of a point $p \in |\Delta|$: the (necessarily finite) set $\{v : p_v \ne 0\}$.

noncomputable def GeometricRealization.vertexRealizationMap {V : Type u_1} [DecidableEq V] [Fintype V] {Δ : SimplicialComplex V} {Z : Type u_2} [AddCommMonoid Z] [Module ℝ Z] (i : V → Z) (p : Point Δ) : Z

Vertex-realization: given a vertex map $i : V \to Z$ into an $\mathbb R$-module, extend to the geometric realization $|\Delta| \to Z$ by barycentric combinations $p \mapsto \sum_v p_v \cdot i(v)$.

structure CoxeterComplexGeometricRealization (W : Type u_1) [Group W] (S : Set W) : Type (max u_1 (u_2 + 1))

An abstract geometric realization of a Coxeter complex $(W, S)$: a topological space carrier together with a $W$-indexed family of "chamber" subsets and a fundamental domain.

• carrier : Type u_2
• topSpace : TopologicalSpace self.carrier
• chamberMap : W → Set self.carrier
• fundamentalDomain : Set self.carrier

structure AffineGeometricRealization (W : Type u_1) [Group W] (S : Set W) (ι : Type u_2) [Fintype ι] : Type (max u_1 u_2)

An affine geometric realization: an action of $W$ by Euclidean transformations of $\mathbb R^\iota$, together with a fundamental chamber, its $W$-translates, and the underlying hyperplane arrangement.

• action : W → EuclideanSpace ℝ ι → EuclideanSpace ℝ ι
• action_mul (w₁ w₂ : W) (x : EuclideanSpace ℝ ι) : self.action (w₁ * w₂) x = self.action w₁ (self.action w₂ x)
• action_one (x : EuclideanSpace ℝ ι) : self.action 1 x = x
• fundamentalChamber : Set (EuclideanSpace ℝ ι)
• chamber (w : W) : Set (EuclideanSpace ℝ ι)
• hyperplanes : Set (Set (EuclideanSpace ℝ ι))

def AffineGeometricRealization.toCoxeterComplex {W : Type u_1} [Group W] {S : Set W} {ι : Type u_2} [Fintype ι] (A : AffineGeometricRealization W S ι) : CoxeterComplexGeometricRealization W S

Forgetting the linear/Euclidean structure: every affine geometric realization gives an abstract geometric realization with the same chambers and fundamental domain.