Geometric realization of an abstract simplicial complex

This file realizes an abstract simplicial complex in the real vector space of finitely supported functions on its vertices. A vertex v is represented by the coordinate vector Finsupp.single v 1; the realization is the union of the convex hulls of the images of the faces. Thus points of the realization are precisely finite barycentric combinations supported on a face.

The construction uses Geometry.SimplicialComplex.onFinsupp from Mathlib, which proves that the standard coordinate vectors are affinely independent and that their convex hulls intersect along common faces. The polyhedron carries the weak topology: the final topology for the inclusions of all its closed simplices. This avoids a finiteness or local-finiteness hypothesis on K.

This is the first item of layer 11 of the geometric-topology roadmap: the polyhedron |K| of an abstract simplicial complex. It is the object used in the subsequent definition of a triangulation.

Main definitions

• AbstractSimplicialComplex.standardGeometricComplex: the standard geometric complex of K.
• AbstractSimplicialComplex.Realization: the topological space underlying its polyhedron.
• AbstractSimplicialComplex.faceBarycenter: the barycenter of a face in standard coordinates.

Main results

• mem_standardGeometricComplex_faces_iff: the geometric faces are exactly the coordinate images of the abstract faces.
• mem_realization_iff: a finitely supported function belongs to the polyhedron exactly when it lies in the convex hull of the coordinate image of some abstract face.
• faceBarycenter_mem: a face barycenter belongs to its closed simplex.
• vertex: the canonical point of the realization corresponding to a vertex.
• realizationBotHomeomorph: the realization of the bottom complex is its discrete vertex space.

noncomputable def AbstractSimplicialComplex.standardGeometricComplex {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Geometry.SimplicialComplex ℝ (ι →₀ ℝ)

The standard geometric simplicial complex associated to an abstract simplicial complex.

Each vertex is sent to its coordinate vector in ι →₀ ℝ. This is Mathlib's Geometry.SimplicialComplex.onFinsupp construction.

Equations

• K.standardGeometricComplex = Geometry.SimplicialComplex.onFinsupp K.toPreAbstractSimplicialComplex

@[reducible, inline]

noncomputable abbrev AbstractSimplicialComplex.Realization {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Type u_1

The carrier of the geometric realization (polyhedron) of an abstract simplicial complex.

Equations

• K.Realization = ↑K.standardGeometricComplex.space

@[reducible, inline]

noncomputable abbrev AbstractSimplicialComplex.StandardSimplex {ι : Type u_1} (σ : Finset ι) : Type u_1

The closed simplex spanned by a finite vertex set, in standard barycentric coordinates.

Equations

• AbstractSimplicialComplex.StandardSimplex σ = ↑((convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) σ))

noncomputable def AbstractSimplicialComplex.faceBarycenter {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : ι →₀ ℝ

The barycenter of a nonempty face, expressed in the standard barycentric coordinates of the realization.

Equations

• K.faceBarycenter σ = Finset.centroid ℝ (Finset.image (fun (v : ι) => Finsupp.single v 1) ↑σ) id

theorem AbstractSimplicialComplex.faceBarycenter_mem {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : K.faceBarycenter σ ∈ (convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) ↑σ)

The barycenter of a face belongs to the closed simplex spanned by that face.

@[simp]

theorem AbstractSimplicialComplex.faceBarycenter_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) (v : ι) : (K.faceBarycenter σ) v = if v ∈ ↑σ then (↑(↑σ).card)⁻¹ else 0

The barycenter of a face has equal coordinates on its vertices and vanishes elsewhere.

@[instance_reducible]

instance AbstractSimplicialComplex.instTopologicalSpaceStandardSimplex {ι : Type u_1} (σ : Finset ι) : TopologicalSpace (StandardSimplex σ)

The topology induced by the coordinatewise topology on ι → ℝ. These are the domain topologies used to define the weak topology on the whole realization.

Equations

• AbstractSimplicialComplex.instTopologicalSpaceStandardSimplex σ = TopologicalSpace.induced (fun (x : AbstractSimplicialComplex.StandardSimplex σ) => ⇑↑x) inferInstance

instance AbstractSimplicialComplex.instCompactSpaceStandardSimplex {ι : Type u_1} (σ : Finset ι) : CompactSpace (StandardSimplex σ)

Every closed coordinate simplex is compact, even in an infinite vertex set.

theorem AbstractSimplicialComplex.mem_standardGeometricComplex_faces_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) (τ : Finset (ι →₀ ℝ)) : τ ∈ K.standardGeometricComplex.faces ↔ ∃ σ ∈ K, Finset.image (fun (v : ι) => Finsupp.single v 1) σ = τ

A geometric face is exactly the image of an abstract face under the coordinate embedding.

noncomputable def AbstractSimplicialComplex.faceInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : StandardSimplex ↑σ → K.Realization

Include the realization of a face into the whole polyhedron.

Equations

• K.faceInclusion σ = Set.inclusion ⋯

@[simp]

theorem AbstractSimplicialComplex.faceInclusion_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) : ↑(K.faceInclusion σ x) = ↑x

A face inclusion does not change the underlying barycentric coordinates.

@[instance_reducible]

noncomputable instance AbstractSimplicialComplex.instTopologicalSpaceRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) : TopologicalSpace K.Realization

The weak topology on a realization, final with respect to all face inclusions.

Equations

• K.instTopologicalSpaceRealization = ⨆ (σ : TauCeti.SetLike.Face K), TopologicalSpace.coinduced (K.faceInclusion σ) inferInstance

theorem AbstractSimplicialComplex.continuous_faceInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : Continuous (K.faceInclusion σ)

Every face inclusion is continuous for the weak topology on the realization.

theorem AbstractSimplicialComplex.isClosed_iff_faceInclusion {ι : Type u_1} {K : AbstractSimplicialComplex ι} {s : Set K.Realization} : IsClosed s ↔ ∀ (σ : TauCeti.SetLike.Face K), IsClosed (K.faceInclusion σ ⁻¹' s)

A subset of a weak realization is closed exactly when its inverse image in every closed simplex is closed.

theorem AbstractSimplicialComplex.continuous_iff_faceInclusion {ι : Type u_1} {K : AbstractSimplicialComplex ι} {X : Type u_2} [TopologicalSpace X] {f : K.Realization → X} : Continuous f ↔ ∀ (σ : TauCeti.SetLike.Face K), Continuous (f ∘ K.faceInclusion σ)

A map out of a realization is continuous exactly when its restriction to every face is continuous.

theorem AbstractSimplicialComplex.continuous_realization_coe {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Continuous fun (x : K.Realization) => ⇑↑x

Barycentric coordinates are continuous for the weak topology, for any vertex type.

theorem AbstractSimplicialComplex.injective_realization_coe {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Function.Injective fun (x : K.Realization) => ⇑↑x

Distinct realization points have distinct barycentric coordinates.

instance AbstractSimplicialComplex.instT2SpaceRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) : T2Space K.Realization

The weak realization is Hausdorff: distinct points have distinct continuous barycentric coordinates.

theorem AbstractSimplicialComplex.image_single_mem_standardGeometricComplex_faces {ι : Type u_1} {K : AbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ ∈ K) : Finset.image (fun (v : ι) => Finsupp.single v 1) σ ∈ K.standardGeometricComplex.faces

The coordinate image of every abstract face is a face of the geometric complex.

theorem AbstractSimplicialComplex.mem_realization_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} {x : ι →₀ ℝ} : x ∈ K.standardGeometricComplex.space ↔ ∃ σ ∈ K, x ∈ (convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) σ)

A point belongs to the standard polyhedron exactly when it lies in the convex hull of the coordinate image of some abstract face.

theorem AbstractSimplicialComplex.StandardSimplex.nonneg {ι : Type u_1} {σ : Finset ι} (x : StandardSimplex σ) (v : ι) : 0 ≤ ↑x v

Barycentric coordinates in a standard simplex are nonnegative.

theorem AbstractSimplicialComplex.StandardSimplex.sum_eq_one {ι : Type u_1} {σ : Finset ι} (x : StandardSimplex σ) : ((↑x).sum fun (x : ι) (r : ℝ) => r) = 1

The barycentric coordinates in a standard simplex sum to one.

theorem AbstractSimplicialComplex.StandardSimplex.support_subset {ι : Type u_1} {σ : Finset ι} (x : StandardSimplex σ) : (↑x).support ⊆ σ

The support of a point in a standard simplex is contained in its vertex set.

@[simp]

theorem AbstractSimplicialComplex.mem_standardSimplex_iff {ι : Type u_1} {σ : Finset ι} {x : ι →₀ ℝ} : x ∈ (convexHull ℝ) ((fun (v : ι) => Finsupp.single v 1) '' ↑σ) ↔ (∀ (v : ι), 0 ≤ x v) ∧ (x.sum fun (x : ι) (r : ℝ) => r) = 1 ∧ x.support ⊆ σ

Membership in a standard simplex in terms of barycentric coordinates.

theorem AbstractSimplicialComplex.StandardSimplex.mem_convexHull_support {ι : Type u_1} {σ : Finset ι} (x : StandardSimplex σ) : ↑x ∈ (convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) (↑x).support)

A point of a standard simplex lies in the simplex spanned by its support.

theorem AbstractSimplicialComplex.support_mem {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : (↑x).support ∈ K

The support of a realization point is an abstract face.

noncomputable def AbstractSimplicialComplex.carrier {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : TauCeti.SetLike.Face K

The minimal abstract face carrying a point of the realization.

Equations

• K.carrier x = ⟨(↑x).support, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.carrier_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : ↑(K.carrier x) = (↑x).support

The vertices of the carrier are exactly the nonzero barycentric coordinates.

theorem AbstractSimplicialComplex.mem_convexHull_carrier {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : ↑x ∈ (convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) ↑(K.carrier x))

A realization point belongs to the closed simplex spanned by its carrier.

theorem AbstractSimplicialComplex.Realization.nonneg {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) (v : ι) : 0 ≤ ↑x v

The barycentric coordinates of a point of the realization are nonnegative.

@[simp]

theorem AbstractSimplicialComplex.Realization.sum_eq_one {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : ((↑x).sum fun (x : ι) (r : ℝ) => r) = 1

The barycentric coordinates of a realization point sum to one.

theorem AbstractSimplicialComplex.Realization.le_one {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) (v : ι) : ↑x v ≤ 1

Every barycentric coordinate of a realization point is at most one.

theorem AbstractSimplicialComplex.carrier_minimal {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) {σ : Finset ι} (hx : ↑x ∈ (convexHull ℝ) ↑(Finset.image (fun (v : ι) => Finsupp.single v 1) σ)) : ↑(K.carrier x) ⊆ σ

The carrier is contained in every finite vertex set whose closed simplex contains the point.

theorem AbstractSimplicialComplex.single_mem_standardGeometricComplex_space {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : Finsupp.single v 1 ∈ K.standardGeometricComplex.space

The standard coordinate vector of every vertex belongs to the geometric realization.

noncomputable def AbstractSimplicialComplex.vertex {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : K.Realization

The canonical point of the geometric realization corresponding to a vertex.

Equations

• K.vertex v = ⟨Finsupp.single v 1, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.vertex_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : ↑(K.vertex v) = Finsupp.single v 1

The underlying finitely supported function of a realization vertex is its coordinate vector.

@[simp]

theorem AbstractSimplicialComplex.Realization.eq_vertex_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) (v : ι) : x = K.vertex v ↔ ↑x v = 1

A realization point is a vertex exactly when its coordinate at that vertex is one.

theorem AbstractSimplicialComplex.vertex_injective {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Function.Injective K.vertex

Distinct vertices give distinct points in the geometric realization.

noncomputable def AbstractSimplicialComplex.vertexEmbedding {ι : Type u_1} (K : AbstractSimplicialComplex ι) : ι ↪ K.Realization

The canonical map from vertices to the realization.

Equations

• K.vertexEmbedding = { toFun := K.vertex, inj' := ⋯ }

@[simp]

theorem AbstractSimplicialComplex.vertexEmbedding_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : K.vertexEmbedding v = K.vertex v

The vertex embedding sends a vertex to its canonical point in the realization.

theorem AbstractSimplicialComplex.vertex_bot_surjective {ι : Type u_1} : Function.Surjective ⊥.vertex

The vertices exhaust the realization of the bottom abstract simplicial complex.

instance AbstractSimplicialComplex.realizationBotDiscreteTopology {ι : Type u_1} : DiscreteTopology ⊥.Realization

The weak topology on the realization of the bottom abstract simplicial complex is discrete.

noncomputable def AbstractSimplicialComplex.realizationBotHomeomorph {ι : Type u_1} [TopologicalSpace ι] [DiscreteTopology ι] : ⊥.Realization ≃ₜ ι

The realization of the bottom abstract simplicial complex is canonically homeomorphic to its vertex type equipped with a discrete topology.

Equations

• AbstractSimplicialComplex.realizationBotHomeomorph = (Homeomorph.ofDiscrete AbstractSimplicialComplex.vertexEquivBot✝).symm

@[simp]

theorem AbstractSimplicialComplex.realizationBotHomeomorph_symm_apply {ι : Type u_1} [TopologicalSpace ι] [DiscreteTopology ι] (v : ι) : realizationBotHomeomorph.symm v = ⊥.vertex v

Under the canonical homeomorphism for the bottom complex, the inverse sends a vertex to its standard barycentric point.

@[simp]

theorem AbstractSimplicialComplex.realizationBotHomeomorph_apply_vertex {ι : Type u_1} [TopologicalSpace ι] [DiscreteTopology ι] (v : ι) : realizationBotHomeomorph (⊥.vertex v) = v

The canonical homeomorphism sends the barycentric point of a vertex back to that vertex.

theorem AbstractSimplicialComplex.standardGeometricComplex_space_mono {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) : K.standardGeometricComplex.space ⊆ L.standardGeometricComplex.space

Inclusion of abstract complexes induces inclusion of their standard polyhedra.

noncomputable def AbstractSimplicialComplex.realizationMap {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) : K.Realization → L.Realization

The continuous map of realizations induced by an inclusion of abstract complexes.

Equations

• AbstractSimplicialComplex.realizationMap hKL = Set.inclusion ⋯

@[simp]

theorem AbstractSimplicialComplex.realizationMap_val {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) (x : K.Realization) : ↑(realizationMap hKL x) = ↑x

An induced map of realizations does not change the underlying barycentric coordinates.

theorem AbstractSimplicialComplex.realizationMap_injective {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) : Function.Injective (realizationMap hKL)

The map of realizations induced by an inclusion is injective.

@[simp]

theorem AbstractSimplicialComplex.realizationMap_comp_faceInclusion {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) (σ : TauCeti.SetLike.Face K) : realizationMap hKL ∘ K.faceInclusion σ = L.faceInclusion ⟨↑σ, ⋯⟩

An inclusion map restricted to a face is the corresponding face inclusion in the larger complex.

theorem AbstractSimplicialComplex.continuous_realizationMap {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (hKL : K ≤ L) : Continuous (realizationMap hKL)

The map of realizations induced by an inclusion is continuous.

@[simp]

theorem AbstractSimplicialComplex.realizationMap_refl {ι : Type u_1} (K : AbstractSimplicialComplex ι) : realizationMap ⋯ = id

The map induced by the reflexive inclusion is the identity.

theorem AbstractSimplicialComplex.realizationMap_trans {ι : Type u_1} {K L M : AbstractSimplicialComplex ι} (hKL : K ≤ L) (hLM : L ≤ M) : realizationMap ⋯ = realizationMap hLM ∘ realizationMap hKL

Maps induced by inclusions compose according to transitivity of inclusion.