Documentation

TauCeti.AlgebraicTopology.SimplicialComplex.Pure

Pure simplicial complexes and dimensions of links #

A complex is pure of dimension n if every face is contained in a face with n + 1 vertices. This formulation works for infinite complexes as well: it gives both a uniform dimension bound and extension to a top-dimensional face. The void complex is pure in every dimension; dimension equalities consequently require nonvoidness.

Links of faces of a pure complex are pure in the complementary dimension. A top-dimensional face has void link, whose dimension is ⊥, rather than a truncated natural-number dimension. These facts provide the dimension indices for sphere-or-ball link classifications.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapters 2--3.

source
def PreAbstractSimplicialComplex.IsPure {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (n : ℕ) :
Prop

A complex is pure of dimension n when every face extends to a face with n + 1 vertices. The void complex satisfies this condition in every dimension.

Equations
Instances For
    source
    theorem PreAbstractSimplicialComplex.isPure_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} :
    K.IsPure n ↔ ∀ σ ∈ K, ∃ τ ∈ K, σ ⊆ τ ∧ τ.card = n + 1

    The coface characterization of purity.

    source
    theorem PreAbstractSimplicialComplex.IsPure.exists_coface {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} {σ : Finset ι} (h : K.IsPure n) (hσ : σ ∈ K) :
    ∃ τ ∈ K, σ ⊆ τ ∧ τ.card = n + 1

    Every face of a pure complex extends to a face of the prescribed dimension.

    source
    theorem PreAbstractSimplicialComplex.IsPure.card_le {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} {σ : Finset ι} (h : K.IsPure n) (hσ : σ ∈ K) :
    σ.card ≤ n + 1

    Every face of a pure n-complex has at most n + 1 vertices.

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

    Purity bounds the dimension, even for the void complex.

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

    A nonvoid pure n-complex has dimension n.

    source
    theorem PreAbstractSimplicialComplex.IsPure.card_eq_of_maximal {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} {σ : Finset ι} (h : K.IsPure n) (hσ : Maximal (fun (x : Finset ι) => x ∈ K) σ) :
    σ.card = n + 1

    A maximal face of a pure n-complex has exactly n + 1 vertices.

    source
    @[simp]
    theorem PreAbstractSimplicialComplex.isPure_map_iff {ι : Type u_1} {κ : Type u_2} {K : PreAbstractSimplicialComplex ι} {n : ℕ} [DecidableEq κ] (f : ι → κ) (hf : Function.Injective f) :
    (K.map f).IsPure n ↔ K.IsPure n

    Injective relabeling preserves and reflects purity, including for infinite vertex types.

    source
    theorem PreAbstractSimplicialComplex.isPure_simplex {ι : Type u_1} {n : ℕ} {V : Finset ι} (hV : V.card = n + 1) :
    (simplex V).IsPure n

    A nonempty simplex is pure of its expected dimension.

    source
    theorem PreAbstractSimplicialComplex.isPure_simplexBoundary {ι : Type u_1} {n : ℕ} {V : Finset ι} (hV : V.card = n + 2) :
    (simplexBoundary V).IsPure n

    The boundary of an (n + 1)-simplex is pure of dimension n.