Additions to the `SimplicialComplex` API

Stream: mathlib4

[Evan Bailey]

I am working on some results for finite/finite-dimensional simplicial complexes which require new definitions. Before I spend too much time, I wanted to make sure that some of the basic definitions I added are sensible.

These are in Geometry.SimplicialComplex:

variable {𝕜 E : Type*} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E}

def facesOfDimension (n : ℕ) : Set (Finset E) := {s ∈ K.faces | #s = n + 1}

noncomputable def dimension : WithBot ℕ∞ := ⨆ s ∈ K.faces, WithBot.some ↑(#s - 1)

noncomputable def natDimension : ℕ := WithTop.untop' 0 (WithBot.unbot' 0 K.dimension)

def Homogeneous (K : SimplicialComplex 𝕜 E) : Prop := ∀ s ∈ K.facets, ↑(#s : ℕ∞) = K.dimension

protected def FiniteDimensional (K : SimplicialComplex 𝕜 E) : Prop := (card '' K.faces).Bounded LE.le

protected def Finite (K : SimplicialComplex 𝕜 E) : Prop := K.faces.Finite

The major concerns I have are:

• It feels like there should be a better name for facesOfDimension.
• How should Homogeneous handle infinite-dimensional complexes? Currently, it allows them iff they have no facets.
• Does it make sense to use WithBot ℕ∞ for dimension, or should the empty complex have dimension 0 instead? This was inspired by Polynomial.degree which returns a WithBot ℕ, but since this uses ℕ∞ instead of just ℕ, coercion is more of a pain. I also saw a thread about using upper sets in ℕ to represent the "has dimension less than" relation instead, but that seems like a significant departure from how other versions of dimension/rank are defined.
• Would it be better to define things in terms of the Krull dimension of an appropriate order structure on the faces?

[Yaël Dillies]

There's more stuff about simplicial complexes here. A better definition of Homogeneous would also stipulate that all faces of dimension at most n