Order complexes

The order complex of a preordered type has the elements of the type as vertices and the nonempty finite chains as faces. This is the general construction underlying barycentric subdivision: applying it to the face poset of a simplicial complex gives its first barycentric subdivision.

This file also records functoriality. A monotone map sends a chain to a chain, and hence induces a simplicial map of order complexes. The barycentric-subdivision specialization in the next module models the derived subdivision described by Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2; the generic order-complex formulation and its functoriality are not taken from that source.

Main definitions

• TauCeti.AbstractSimplicialComplex.orderComplex: the simplicial complex of nonempty finite chains.
• TauCeti.AbstractSimplicialComplex.orderComplexMap: the simplicial map induced by a monotone map.

Main results

• TauCeti.AbstractSimplicialComplex.mem_orderComplex_iff: faces are exactly the nonempty finite chains.
• TauCeti.AbstractSimplicialComplex.pair_mem_orderComplex_iff: two vertices span an edge exactly when they are comparable.
• TauCeti.AbstractSimplicialComplex.orderComplex_eq_top: the order complex of a total preorder is the full simplicial complex.
• TauCeti.AbstractSimplicialComplex.orderComplexMap_id and TauCeti.AbstractSimplicialComplex.orderComplexMap_comp: functoriality laws.

noncomputable def TauCeti.AbstractSimplicialComplex.orderComplex (P : Type u_4) [Preorder P] : AbstractSimplicialComplex P

The order complex of a preordered type P. Its vertices are the elements of P, and a nonempty finite set of vertices is a face exactly when its elements are pairwise comparable.

Equations

• TauCeti.AbstractSimplicialComplex.orderComplex P = { faces := {σ : Finset P | σ.Nonempty ∧ IsChain (fun (x1 x2 : P) => x1 ≤ x2) ↑σ}, isRelLowerSet_faces := ⋯, singleton_mem := ⋯ }

@[simp]

theorem TauCeti.AbstractSimplicialComplex.mem_orderComplex_iff {P : Type u_1} [Preorder P] {σ : Finset P} : σ ∈ orderComplex P ↔ σ.Nonempty ∧ IsChain (fun (x1 x2 : P) => x1 ≤ x2) ↑σ

A finite set is a face of the order complex exactly when it is nonempty and is a chain.

theorem TauCeti.AbstractSimplicialComplex.mem_orderComplex_iff' {P : Type u_1} [Preorder P] {σ : Finset P} : σ ∈ orderComplex P ↔ σ.Nonempty ∧ ∀ p ∈ σ, ∀ q ∈ σ, p ≤ q ∨ q ≤ p

A finite set is a face of the order complex exactly when it is nonempty and every two of its elements are comparable.

theorem TauCeti.AbstractSimplicialComplex.le_or_le_of_mem_orderComplex {P : Type u_1} [Preorder P] {σ : Finset P} (hσ : σ ∈ orderComplex P) {p q : P} (hp : p ∈ σ) (hq : q ∈ σ) : p ≤ q ∨ q ≤ p

In a face of an order complex, every two vertices are comparable.

theorem TauCeti.AbstractSimplicialComplex.pair_mem_orderComplex_iff {P : Type u_1} [Preorder P] [DecidableEq P] (p q : P) : {p, q} ∈ orderComplex P ↔ p ≤ q ∨ q ≤ p

Two elements span an edge of the order complex exactly when they are comparable. This also covers the degenerate case p = q, when the pair is a singleton face.

This is not a simp lemma: mem_orderComplex_iff already rewrites the left-hand side.

@[simp]

theorem TauCeti.AbstractSimplicialComplex.orderComplex_eq_top (P : Type u_4) [Preorder P] [Std.Total fun (x1 x2 : P) => x1 ≤ x2] : orderComplex P = ⊤

If the preorder on P is total, every nonempty finite set is a chain, so its order complex is the full abstract simplicial complex.

def TauCeti.AbstractSimplicialComplex.orderComplexMap {P : Type u_1} {Q : Type u_2} [Preorder P] [Preorder Q] [DecidableEq Q] (f : P →o Q) : (orderComplex P).SimplicialMap (orderComplex Q).toPreAbstractSimplicialComplex

A monotone map induces a simplicial map between order complexes.

Equations

• TauCeti.AbstractSimplicialComplex.orderComplexMap f = { toFun := ⇑f, map_face' := ⋯ }

@[simp]

theorem TauCeti.AbstractSimplicialComplex.coe_orderComplexMap {P : Type u_1} {Q : Type u_2} [Preorder P] [Preorder Q] [DecidableEq Q] (f : P →o Q) : ⇑(orderComplexMap f) = ⇑f

@[simp]

theorem TauCeti.AbstractSimplicialComplex.orderComplexMap_apply {P : Type u_1} {Q : Type u_2} [Preorder P] [Preorder Q] [DecidableEq Q] (f : P →o Q) (p : P) : (orderComplexMap f) p = f p

@[simp]

theorem TauCeti.AbstractSimplicialComplex.orderComplexMap_id {P : Type u_1} [Preorder P] [DecidableEq P] : orderComplexMap OrderHom.id = PreAbstractSimplicialComplex.SimplicialMap.id (orderComplex P).toPreAbstractSimplicialComplex

The simplicial map of order complexes induced by the identity is the identity simplicial map.

@[simp]

theorem TauCeti.AbstractSimplicialComplex.orderComplexMap_comp {P : Type u_1} {Q : Type u_2} {R : Type u_3} [Preorder P] [Preorder Q] [Preorder R] [DecidableEq Q] [DecidableEq R] (g : Q →o R) (f : P →o Q) : orderComplexMap (g.comp f) = (orderComplexMap g).comp (orderComplexMap f)

The simplicial map of order complexes induced by a composite is the composite of the induced simplicial maps.