Basic abstract simplicial complex API

This file contains general-purpose lemmas supplementing Mathlib's basic abstract simplicial complex API.

Faces are bundled by TauCeti.SetLike.Face, stated for an arbitrary set-like collection of finite sets so that the same type describes the faces of an AbstractSimplicialComplex and of a PreAbstractSimplicialComplex; hence its neutral namespace.

@[reducible, inline]

abbrev TauCeti.SetLike.Face {ι : Type u_1} {S : Type u_2} [SetLike S (Finset ι)] (K : S) : Type u_1

A face of a set-like collection of finite sets, bundled with its membership proof.

Equations

• TauCeti.SetLike.Face K = ↥K

theorem TauCeti.SetLike.face_le_iff {ι : Type u_1} {S : Type u_2} [SetLike S (Finset ι)] {K : S} {σ τ : Face K} : σ ≤ τ ↔ ↑σ ⊆ ↑τ

The order on bundled faces is inclusion of their underlying finite sets.

@[simp]

theorem AbstractSimplicialComplex.mem_toPreAbstractSimplicialComplex {ι : Type u_1} {K : AbstractSimplicialComplex ι} {σ : Finset ι} : σ ∈ K.toPreAbstractSimplicialComplex ↔ σ ∈ K

A finite set is a face of the underlying precomplex exactly when it is a face of the abstract simplicial complex itself. This is the single place where the two SetLike instances are identified.

theorem PreAbstractSimplicialComplex.mem_map_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] {f : ι → κ} {τ : Finset κ} : τ ∈ K.map f ↔ ∃ σ ∈ K, Finset.image f σ = τ

A face belongs to the image complex exactly when it is the image of a face of the source complex.

theorem PreAbstractSimplicialComplex.faces_map {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (f : ι → κ) : (K.map f).faces = (fun (σ : Finset ι) => Finset.image f σ) '' K.faces

The face set of an image complex is the direct image of the source face set.

@[simp]

theorem PreAbstractSimplicialComplex.map_map {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {κ : Type u_2} {μ : Type u_3} [DecidableEq κ] [DecidableEq μ] (f : ι → κ) (g : κ → μ) : (K.map f).map g = K.map (g ∘ f)

Successive vertex maps agree with mapping by their composite.

@[simp]

theorem PreAbstractSimplicialComplex.map_id {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} [DecidableEq ι] : K.map id = K

The identity vertex map leaves a complex unchanged.

theorem PreAbstractSimplicialComplex.finite_faces_map_iff_of_injective {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (f : ι → κ) (hf : Function.Injective f) : (K.map f).faces.Finite ↔ K.faces.Finite

An injective relabeling preserves and reflects finiteness of the face collection.

@[simp]

theorem PreAbstractSimplicialComplex.mem_inf {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {ρ : Finset ι} : ρ ∈ K ⊓ L ↔ ρ ∈ K ∧ ρ ∈ L

A finite set is a face of an intersection of two precomplexes exactly when it is a face of both.

theorem PreAbstractSimplicialComplex.singleton_mem_of_mem {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : v ∈ σ) : {v} ∈ K

Every vertex of a face spans a singleton face.

theorem PreAbstractSimplicialComplex.notMem_of_singleton_notMem {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) (hσ : σ ∈ K) : v ∉ σ

A vertex whose singleton is not a face occurs in no face at all. This is the convenient way to say that a vertex is unused by a complex, as needed when a construction adjoins a fresh vertex.

theorem TauCeti.AbstractSimplicialComplex.mem_top_iff {ι : Type u_1} {σ : Finset ι} : σ ∈ ⊤ ↔ σ.Nonempty

A finite set belongs to the full abstract simplicial complex exactly when it is nonempty.