Documentation

TauCeti.AlgebraicTopology.SimplicialComplex.CombinatorialManifold.Basic

Combinatorial balls, spheres, and manifolds #

A simplicial complex is a combinatorial n-ball when it is stellar equivalent to the standard n-simplex, and a combinatorial n-sphere when it is stellar equivalent to the boundary of the standard (n+1)-simplex. A complex is a combinatorial n-manifold when the link of each of its vertices is a combinatorial (n-1)-sphere — an interior vertex — or a combinatorial (n-1)-ball — a boundary vertex. This is the simplicial side of piecewise-linear topology asked for by layer 11 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md), the definition that "has the correct links to be a manifold".

The models are the complexes of Simplex.Basic: simplex V for a vertex set of n + 1 elements, and simplexBoundary V for one of n + 2 elements, so that both models have dimension n. They are compared using PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling, which injectively relabels both complexes in a common enlarged vertex type; the comparison relation therefore quantifies over the chosen vertex names.

The dimension convention, and why 0 is a separate case #

IsCombinatorialManifold is defined by cases on the dimension rather than through a truncated subtraction. The link of a vertex of a 0-manifold — a discrete set of points — is the void complex, which is neither a combinatorial ball nor a combinatorial sphere in any dimension ≥ 0; writing the link condition with n - 1 in ℕ would therefore make the 0-dimensional case silently wrong rather than merely unused. The two cases are exposed by PreAbstractSimplicialComplex.isCombinatorialManifold_zero_iff and PreAbstractSimplicialComplex.isCombinatorialManifold_succ_iff.

Main definitions #

Main results #

References #

Combinatorial balls and spheres #

source
def PreAbstractSimplicialComplex.IsCombinatorialBall {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (n : ℕ) :
Prop

K is a combinatorial n-ball when it is stellar equivalent up to relabeling to the simplex on some (n + 1)-element vertex set, the standard n-simplex.

Equations
Instances For
    source
    def PreAbstractSimplicialComplex.IsCombinatorialSphere {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (n : ℕ) :
    Prop

    K is a combinatorial n-sphere when it is stellar equivalent up to relabeling to the boundary of the simplex on some (n + 2)-element vertex set, the boundary of the standard (n+1)-simplex.

    Equations
    Instances For
      source
      theorem PreAbstractSimplicialComplex.isCombinatorialBall_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} :
      K.IsCombinatorialBall n ↔ ∃ (V : Finset ι), V.card = n + 1 ∧ K.StellarEquivalentUpToRelabeling (simplex V)

      The witness characterization of a combinatorial ball.

      source
      theorem PreAbstractSimplicialComplex.isCombinatorialSphere_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} :
      K.IsCombinatorialSphere n ↔ ∃ (V : Finset ι), V.card = n + 2 ∧ K.StellarEquivalentUpToRelabeling (simplexBoundary V)

      The witness characterization of a combinatorial sphere.

      source
      theorem PreAbstractSimplicialComplex.isCombinatorialBall_simplex {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {n : ℕ} (hV : V.card = n + 1) :
      (simplex V).IsCombinatorialBall n

      The standard n-simplex is a combinatorial n-ball, with no moves needed.

      source
      theorem PreAbstractSimplicialComplex.isCombinatorialSphere_simplexBoundary {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {n : ℕ} (hV : V.card = n + 2) :
      (simplexBoundary V).IsCombinatorialSphere n

      The boundary of the standard (n+1)-simplex is a combinatorial n-sphere, with no moves needed.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialBall.of_stellarEquivalentUpToRelabeling {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.StellarEquivalentUpToRelabeling L) (hL : L.IsCombinatorialBall n) :
      K.IsCombinatorialBall n

      Being a combinatorial ball transfers along an intrinsic stellar equivalence.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.of_stellarEquivalentUpToRelabeling {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.StellarEquivalentUpToRelabeling L) (hL : L.IsCombinatorialSphere n) :
      K.IsCombinatorialSphere n

      Being a combinatorial sphere transfers along an intrinsic stellar equivalence.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialBall.stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} {v : ι} {σ : Finset ι} (h : K.IsCombinatorialBall n) (hσ : σ ∈ K) (hv : {v} ∉ K) :
      (K.stellarSubdivision σ v).IsCombinatorialBall n

      Starring a face of a combinatorial ball at a fresh vertex gives another combinatorial ball.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} {v : ι} {σ : Finset ι} (h : K.IsCombinatorialSphere n) (hσ : σ ∈ K) (hv : {v} ∉ K) :
      (K.stellarSubdivision σ v).IsCombinatorialSphere n

      Starring a face of a combinatorial sphere at a fresh vertex gives another combinatorial sphere.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialBall.dimension_eq {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialBall n) :
      K.dimension = ↑n

      A combinatorial n-ball has dimension n.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.dimension_eq {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialSphere n) :
      K.dimension = ↑n

      A combinatorial n-sphere has dimension n.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialBall.finite_faces {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialBall n) :
      K.faces.Finite

      A combinatorial ball has finitely many faces.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.finite_faces {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialSphere n) :
      K.faces.Finite

      A combinatorial sphere has finitely many faces.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialBall.ne_bot {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialBall n) :
      K ≠ ⊥

      A combinatorial ball has a face; in particular it is not the void complex.

      source
      theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.ne_bot {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialSphere n) :
      K ≠ ⊥

      A combinatorial sphere has a face; in particular it is not the void complex.

      Combinatorial manifolds #

      source
      def PreAbstractSimplicialComplex.IsCombinatorialManifold {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) :
      ℕ → Prop

      K is a combinatorial n-manifold when the link of each of its vertices is a combinatorial (n-1)-sphere (an interior vertex) or a combinatorial (n-1)-ball (a boundary vertex).

      The dimension is matched against rather than decremented: in dimension 0 the condition is that every vertex has void link, which is what a discrete set of points satisfies, and which no combinatorial ball or sphere does.

      Equations
      Instances For
        source
        theorem PreAbstractSimplicialComplex.isCombinatorialManifold_zero_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} :
        K.IsCombinatorialManifold 0 ↔ ∀ ⦃v : ι⦄, {v} ∈ K → K.link {v} = ⊥

        In dimension 0 the link condition says that every vertex has void link.

        source
        theorem PreAbstractSimplicialComplex.isCombinatorialManifold_succ_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} :
        K.IsCombinatorialManifold (n + 1) ↔ ∀ ⦃v : ι⦄, {v} ∈ K → (K.link {v}).IsCombinatorialSphere n ∨ (K.link {v}).IsCombinatorialBall n

        In positive dimension the link condition says that every vertex link is a combinatorial sphere or ball one dimension down.

        source
        theorem PreAbstractSimplicialComplex.isCombinatorialManifold_simplex {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {n : ℕ} (hV : V.card = n + 1) :
        (simplex V).IsCombinatorialManifold n

        The standard n-simplex is a combinatorial n-manifold.

        source
        theorem PreAbstractSimplicialComplex.isCombinatorialManifold_simplexBoundary {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {n : ℕ} (hV : V.card = n + 2) :
        (simplexBoundary V).IsCombinatorialManifold n

        The boundary of the standard (n+1)-simplex is a combinatorial n-manifold.

        source
        theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.dimension_le {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialManifold n) :
        K.dimension ≤ ↑n

        A combinatorial n-manifold has dimension at most n.

        source
        theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.dimension_eq {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialManifold n) (hK : K ≠ ⊥) :
        K.dimension = ↑n

        A nonvoid combinatorial n-manifold has dimension exactly n.

        source
        theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.finite_faces_closedStar {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialManifold n) (v : ι) :
        (K.closedStar {v}).faces.Finite

        Every vertex star in a combinatorial manifold has finitely many faces. This includes zero-dimensional manifolds, whose vertex links are void.