Simplicial complexes from affinely independent points

This file provides constructions for simplicial complexes where the vertices are affinely independent.

Main declarations

• Geometry.SimplicialComplex.ofAffineIndependent: Construct a simplicial complex from a downward-closed set of faces whose union of vertices is affinely independent.
• Geometry.SimplicialComplex.onFinsupp: Construct a simplicial complex on ι →₀ 𝕜 from a downward-closed set of finite subsets of ι, using the standard basis vectors.
• Geometry.SimplicialComplex.ofSimpleGraph: Construct a simplicial complex from a simple graph, where vertices of the graph are 0-simplices and edges are 1-simplices.

def Geometry.AbstractSimplicialComplex.ofSimpleGraph {ι : Type u_1} [DecidableEq ι] (G : SimpleGraph ι) : AbstractSimplicialComplex ι

Construct an abstract simplicial complex from a simple graph, where vertices of the graph are 0-simplices and edges are 1-simplices.

Equations

• Geometry.AbstractSimplicialComplex.ofSimpleGraph G = { faces := {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet, isRelLowerSet_faces := ⋯, singleton_mem := ⋯ }

def Geometry.SimplicialComplex.ofAffineIndependent {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq E] [AddCommGroup E] [Module 𝕜 E] (abstract : PreAbstractSimplicialComplex E) (indep : AffineIndependent 𝕜 Subtype.val) : SimplicialComplex 𝕜 E

Construct a simplicial complex from a PreAbstractSimplicialComplex on a set of points in a space, under the assumption that the union of the defining points is affinely independent.

Equations

• Geometry.SimplicialComplex.ofAffineIndependent abstract indep = { toPreAbstractSimplicialComplex := abstract, indep := ⋯, inter_subset_convexHull := ⋯ }

noncomputable def Geometry.SimplicialComplex.onFinsupp {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [DecidableEq 𝕜] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (abstract : PreAbstractSimplicialComplex ι) : SimplicialComplex 𝕜 (ι →₀ 𝕜)

Construct a simplicial complex from an abstract simplicial complex on a set of points over the 𝕜-module of finitely supported functions on those points.

Equations

• Geometry.SimplicialComplex.onFinsupp abstract = Geometry.SimplicialComplex.ofAffineIndependent (abstract.map fun (i : ι) => Finsupp.single i 1) ⋯

noncomputable def Geometry.SimplicialComplex.ofSimpleGraph {𝕜 : Type u_1} {V : Type u_2} [DecidableEq V] [DecidableEq 𝕜] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph V) : SimplicialComplex 𝕜 (V →₀ 𝕜)

The simplicial complex associated to a simple graph, where vertices of the graph are 0-simplices and edges are 1-simplices. The complex is constructed over the 𝕜-module of finitely supported functions on the vertex type.

Equations

• Geometry.SimplicialComplex.ofSimpleGraph G = Geometry.SimplicialComplex.onFinsupp (Geometry.AbstractSimplicialComplex.ofSimpleGraph G).toPreAbstractSimplicialComplex