Abstract Simplicial complexes

In this file, we define abstract simplicial complexes. An abstract simplicial complex is a downwards-closed collection of nonempty finite sets containing every singleton. These are defined first defining PreAbstractSimplicialComplex, which does not require the presence of singletons, and then defining AbstractSimplicialComplex as an extension.

This is related to the geometrical notion of simplicial complexes, which are then defined under the name Geometry.SimplicialComplex using affine combinations in another file.

Main declarations

• PreAbstractSimplicialComplex ι: An abstract simplicial complex with vertices of type ι.
• AbstractSimplicialComplex ι: An abstract simplicial complex with vertices of type ι which contains all singletons.

Notation

• s ∈ K means that s is a face of K. This notation arises from a SetLike instance.
• K ≤ L means that the faces of K are faces of L.

structure PreAbstractSimplicialComplex (ι : Type u_1) : Type u_1

An abstract simplicial complex is a collection of nonempty finite sets of points ("faces") which is downwards closed, i.e., any nonempty subset of a face is also a face.

• faces : Set (Finset ι)

  the faces of this simplicial complex: currently, given by their spanning vertices

• isRelLowerSet_faces : IsRelLowerSet self.faces Finset.Nonempty

  Faces are nonempty and downward closed: a non-empty subset of its spanning vertices spans another face.

theorem PreAbstractSimplicialComplex.ext {ι : Type u_1} {x y : PreAbstractSimplicialComplex ι} (faces : x.faces = y.faces) : x = y

theorem PreAbstractSimplicialComplex.ext_iff {ι : Type u_1} {x y : PreAbstractSimplicialComplex ι} : x = y ↔ x.faces = y.faces

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instSetLikeFinset (ι : Type u_1) : SetLike (PreAbstractSimplicialComplex ι) (Finset ι)

Equations

• PreAbstractSimplicialComplex.instSetLikeFinset ι = { coe := fun (K : PreAbstractSimplicialComplex ι) => K.faces, coe_injective' := ⋯ }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instMin (ι : Type u_1) : Min (PreAbstractSimplicialComplex ι)

The complex consisting of only the faces present in both of its arguments.

Equations

• PreAbstractSimplicialComplex.instMin ι = { min := fun (K L : PreAbstractSimplicialComplex ι) => { faces := K.faces ∩ L.faces, isRelLowerSet_faces := ⋯ } }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instMax (ι : Type u_1) : Max (PreAbstractSimplicialComplex ι)

The complex consisting of all faces present in either of its arguments.

Equations

• PreAbstractSimplicialComplex.instMax ι = { max := fun (K L : PreAbstractSimplicialComplex ι) => { faces := K.faces ∪ L.faces, isRelLowerSet_faces := ⋯ } }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instLE (ι : Type u_1) : LE (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instLE ι = { le := fun (K L : PreAbstractSimplicialComplex ι) => K.faces ⊆ L.faces }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instLT (ι : Type u_1) : LT (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instLT ι = { lt := fun (K L : PreAbstractSimplicialComplex ι) => K.faces ⊂ L.faces }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instPartialOrder (ι : Type u_1) : PartialOrder (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instPartialOrder ι = PartialOrder.lift (fun (K : PreAbstractSimplicialComplex ι) => K.faces) ⋯

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instSupSet (ι : Type u_1) : SupSet (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instSupSet ι = { sSup := fun (s : Set (PreAbstractSimplicialComplex ι)) => { faces := ⋃ K ∈ s, K.faces, isRelLowerSet_faces := ⋯ } }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instInfSet (ι : Type u_1) : InfSet (PreAbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instTop (ι : Type u_1) : Top (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instTop ι = { top := { faces := {s : Finset ι | s.Nonempty}, isRelLowerSet_faces := ⋯ } }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instBot (ι : Type u_1) : Bot (PreAbstractSimplicialComplex ι)

Equations

• PreAbstractSimplicialComplex.instBot ι = { bot := { faces := {_s : Finset ι | False}, isRelLowerSet_faces := ⋯ } }

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instCompleteSemilatticeSup (ι : Type u_1) : CompleteSemilatticeSup (PreAbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instCompleteSemilatticeInf (ι : Type u_1) : CompleteSemilatticeInf (PreAbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PreAbstractSimplicialComplex.instCompleteLattice (ι : Type u_1) : CompleteLattice (PreAbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

def PreAbstractSimplicialComplex.map {α : Type u_2} {β : Type u_3} [DecidableEq β] (K : PreAbstractSimplicialComplex α) (f : α → β) : PreAbstractSimplicialComplex β

Map each vertex in each face of a PreAbstractSimplicialComplex through a function, producing a new PreAbstractSimplicialComplex.

Equations

• K.map f = { faces := (fun (s : Finset α) => Finset.image f s) '' K.faces, isRelLowerSet_faces := ⋯ }

structure AbstractSimplicialComplex (ι : Type u_1) extends PreAbstractSimplicialComplex ι : Type u_1

An AbstractSimplicialComplex is a PreAbstractSimplicialComplex which contains all singletons.

• faces : Set (Finset ι)
• isRelLowerSet_faces : IsRelLowerSet self.faces Finset.Nonempty
• singleton_mem (v : ι) : {v} ∈ self.faces

  every singleton is a face

theorem AbstractSimplicialComplex.ext {ι : Type u_1} {x y : AbstractSimplicialComplex ι} (faces : x.faces = y.faces) : x = y

theorem AbstractSimplicialComplex.ext_iff {ι : Type u_1} {x y : AbstractSimplicialComplex ι} : x = y ↔ x.faces = y.faces

def PreAbstractSimplicialComplex.toAbstractSimplicialComplex (ι : Type u_1) (K : PreAbstractSimplicialComplex ι) (h : ∀ (v : ι), {v} ∈ K.faces) : AbstractSimplicialComplex ι

Convert a PreAbstractSimplicialComplex satisfying IsAbstract to an AbstractSimplicialComplex.

Equations

• PreAbstractSimplicialComplex.toAbstractSimplicialComplex ι K h = { toPreAbstractSimplicialComplex := K, singleton_mem := h }

def PreAbstractSimplicialComplex.addSingletons (ι : Type u_1) (K : PreAbstractSimplicialComplex ι) : AbstractSimplicialComplex ι

The closure of a PreAbstractSimplicialComplex to an AbstractSimplicialComplex by adding all singletons.

Equations

• PreAbstractSimplicialComplex.addSingletons ι K = { faces := K.faces ∪ {s : Finset ι | ∃ (v : ι), s = {v}}, isRelLowerSet_faces := ⋯, singleton_mem := ⋯ }

@[implicit_reducible]

instance AbstractSimplicialComplex.instSetLikeFinset {ι : Type u_1} : SetLike (AbstractSimplicialComplex ι) (Finset ι)

Equations

• AbstractSimplicialComplex.instSetLikeFinset = { coe := fun (K : AbstractSimplicialComplex ι) => K.faces, coe_injective' := ⋯ }

@[implicit_reducible]

instance AbstractSimplicialComplex.instMin {ι : Type u_1} : Min (AbstractSimplicialComplex ι)

The complex consisting of only the faces present in both of its arguments.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instMax {ι : Type u_1} : Max (AbstractSimplicialComplex ι)

The complex consisting of all faces present in either of its arguments.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instLE {ι : Type u_1} : LE (AbstractSimplicialComplex ι)

Equations

• AbstractSimplicialComplex.instLE = { le := fun (K L : AbstractSimplicialComplex ι) => K.faces ⊆ L.faces }

@[implicit_reducible]

instance AbstractSimplicialComplex.instLT {ι : Type u_1} : LT (AbstractSimplicialComplex ι)

Equations

• AbstractSimplicialComplex.instLT = { lt := fun (K L : AbstractSimplicialComplex ι) => K.faces ⊂ L.faces }

@[implicit_reducible]

instance AbstractSimplicialComplex.instPartialOrder {ι : Type u_1} : PartialOrder (AbstractSimplicialComplex ι)

Equations

• AbstractSimplicialComplex.instPartialOrder = PartialOrder.lift (fun (K : AbstractSimplicialComplex ι) => K.faces) ⋯

theorem AbstractSimplicialComplex.toPreAbstractSimplicialComplex_injective {ι : Type u_1} : Function.Injective toPreAbstractSimplicialComplex

@[simp]

theorem AbstractSimplicialComplex.toPreAbstractSimplicialComplex_le_iff {ι : Type u_1} {K L : AbstractSimplicialComplex ι} : K.toPreAbstractSimplicialComplex ≤ L.toPreAbstractSimplicialComplex ↔ K ≤ L

@[simp]

theorem AbstractSimplicialComplex.toPreAbstractSimplicialComplex_lt_iff {ι : Type u_1} {K L : AbstractSimplicialComplex ι} : K.toPreAbstractSimplicialComplex < L.toPreAbstractSimplicialComplex ↔ K < L

@[implicit_reducible]

instance AbstractSimplicialComplex.instSupSet {ι : Type u_1} : SupSet (AbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instInfSet {ι : Type u_1} : InfSet (AbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instTop {ι : Type u_1} : Top (AbstractSimplicialComplex ι)

Equations

• AbstractSimplicialComplex.instTop = { top := let __src := ⊤; { toPreAbstractSimplicialComplex := __src, singleton_mem := ⋯ } }

theorem AbstractSimplicialComplex.top_toPreAbstractSimplicialComplex {ι : Type u_1} : ⊤.toPreAbstractSimplicialComplex = ⊤

@[implicit_reducible]

instance AbstractSimplicialComplex.instBot {ι : Type u_1} : Bot (AbstractSimplicialComplex ι)

Equations

• AbstractSimplicialComplex.instBot = { bot := { faces := {s : Finset ι | ∃ (v : ι), s = {v}}, isRelLowerSet_faces := ⋯, singleton_mem := ⋯ } }

@[implicit_reducible]

instance AbstractSimplicialComplex.instCompleteSemilatticeSup {ι : Type u_1} : CompleteSemilatticeSup (AbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instCompleteSemilatticeInf {ι : Type u_1} : CompleteSemilatticeInf (AbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance AbstractSimplicialComplex.instCompleteLattice {ι : Type u_1} : CompleteLattice (AbstractSimplicialComplex ι)

Equations

• One or more equations did not get rendered due to their size.