Restricting the vertices of a simplicial complex

The restriction of an abstract simplicial complex to a set of vertices is a complex on that set as a subtype. Its faces are precisely the original faces using only those vertices. The subtype inclusion is simplicial; in particular, finite vertex restrictions give finite models inside arbitrary complexes without adjoining unused ambient vertices.

def AbstractSimplicialComplex.restrict {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) : AbstractSimplicialComplex ↑s

Restrict a complex to a set of vertices, changing the vertex type to that set.

@[simp]

theorem AbstractSimplicialComplex.mem_restrict_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (σ : Finset ↑s) : σ ∈ K.restrict s ↔ Finset.image Subtype.val σ ∈ K

A face in the restriction is a face after forgetting the vertex-membership proofs.

def AbstractSimplicialComplex.restrictInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) : (K.restrict s).SimplicialMap K.toPreAbstractSimplicialComplex

The canonical simplicial inclusion of a vertex restriction into the original complex.

@[simp]

theorem AbstractSimplicialComplex.coe_restrictInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) : ⇑(K.restrictInclusion s) = Subtype.val

def AbstractSimplicialComplex.restrictInclusionOfSubset {ι : Type u_1} (K : AbstractSimplicialComplex ι) {s t : Set ι} (hst : s ⊆ t) : (K.restrict s).SimplicialMap (K.restrict t).toPreAbstractSimplicialComplex

The simplicial inclusion between vertex restrictions induced by an inclusion of vertex sets.

@[simp]

theorem AbstractSimplicialComplex.coe_restrictInclusionOfSubset {ι : Type u_1} (K : AbstractSimplicialComplex ι) {s t : Set ι} (hst : s ⊆ t) : ⇑(K.restrictInclusionOfSubset hst) = Set.inclusion hst

The inclusion between vertex restrictions acts on vertices by Set.inclusion.

@[simp]

theorem AbstractSimplicialComplex.restrictInclusion_comp_restrictInclusionOfSubset {ι : Type u_1} (K : AbstractSimplicialComplex ι) {s t : Set ι} (hst : s ⊆ t) : (K.restrictInclusion t).comp (K.restrictInclusionOfSubset hst) = K.restrictInclusion s

Including a smaller vertex restriction into a larger one and then into the original complex is the inclusion of the smaller restriction.

@[simp]

theorem AbstractSimplicialComplex.mem_map_restrict_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (σ : Finset ι) : σ ∈ (K.restrict s).map Subtype.val ↔ σ ∈ K ∧ ↑σ ⊆ s

Relabeling the restricted complex into the original vertex type gives exactly the faces of the original complex contained in the chosen set.