Ordered products of abstract simplicial complexes

The ordered product of two simplicial complexes is the standard staircase triangulation of their product. Its vertices are pairs of vertices. A finite set of pairs is a face when both coordinate projections are faces and the pairs form a chain for the coordinatewise order. The chain condition is essential: without it, the four vertices of a square would span a tetrahedron rather than two triangles.

This file constructs the product first for PreAbstractSimplicialComplex, then for AbstractSimplicialComplex. It also supplies the simplicial coordinate projections, fixed-coordinate inclusions, and the ordered cylinder obtained by taking the second factor to be the standard one-simplex on Fin 2.

The construction is the simplicial product used in the collapse track of layer 11 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md). In particular, the ordered cylinder is the missing product K × I in the statement of Zeeman's conjecture. The definition follows the ordered (staircase) triangulation convention in Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. No claim about the realization of this product is made here; identifying its realization with the product of realizations is later work.

Main definitions

• PreAbstractSimplicialComplex.orderedProd: the ordered product of two precomplexes.
• AbstractSimplicialComplex.orderedProd: the ordered product of two complexes.
• AbstractSimplicialComplex.orderedCylinder: product with the standard one-simplex.
• AbstractSimplicialComplex.isCone_orderedCylinder_of_isCone: taking the ordered cylinder preserves a cone whose apex is greatest.
• PreAbstractSimplicialComplex.SimplicialMap.orderedProdFst and orderedProdSnd: the coordinate projections.
• PreAbstractSimplicialComplex.SimplicialMap.prodMkLeft and prodMkRight: fixed-coordinate inclusions into an ordered product.

def PreAbstractSimplicialComplex.orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : PreAbstractSimplicialComplex (α × β)

The ordered product of two pre-abstract simplicial complexes.

A finite set of pairs is a face exactly when its two coordinate images are faces of the factors and it is a chain for the coordinatewise order on the product. The linear orders are data in the construction: changing them can change the triangulation, though not its intended PL type.

Equations

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

@[simp]

theorem PreAbstractSimplicialComplex.mem_orderedProd_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset (α × β)} : σ ∈ K.orderedProd L ↔ Finset.image Prod.fst σ ∈ K ∧ Finset.image Prod.snd σ ∈ L ∧ IsChain (fun (x1 x2 : α × β) => x1 ≤ x2) ↑σ

Membership in an ordered product is characterized by the two projected face conditions and the staircase chain condition.

theorem PreAbstractSimplicialComplex.image_fst_mem_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : Finset.image Prod.fst σ ∈ K

The first-coordinate image of a face of an ordered product is a face of the first factor.

theorem PreAbstractSimplicialComplex.image_snd_mem_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : Finset.image Prod.snd σ ∈ L

The second-coordinate image of a face of an ordered product is a face of the second factor.

theorem PreAbstractSimplicialComplex.isChain_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : IsChain (fun (x1 x2 : α × β) => x1 ≤ x2) ↑σ

Every face of an ordered product is a chain for the coordinatewise order.

theorem PreAbstractSimplicialComplex.orderedProd_mono {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K K' : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (hK : K ≤ K') (hL : L ≤ L') : K.orderedProd L ≤ K'.orderedProd L'

Ordered product is monotone in both factors.

def PreAbstractSimplicialComplex.SimplicialMap.orderedProdFst {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : (K.orderedProd L).SimplicialMap K

The first coordinate projection from an ordered product is simplicial.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.orderedProdFst K L = { toFun := Prod.fst, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_orderedProdFst {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : ⇑(orderedProdFst K L) = Prod.fst

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.orderedProdFst_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (p : α × β) : (orderedProdFst K L) p = p.1

def PreAbstractSimplicialComplex.SimplicialMap.orderedProdSnd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : (K.orderedProd L).SimplicialMap L

The second coordinate projection from an ordered product is simplicial.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.orderedProdSnd K L = { toFun := Prod.snd, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_orderedProdSnd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : ⇑(orderedProdSnd K L) = Prod.snd

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.orderedProdSnd_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (p : α × β) : (orderedProdSnd K L) p = p.2

def PreAbstractSimplicialComplex.SimplicialMap.prodMkLeft {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (b : β) (hb : {b} ∈ L) : K.SimplicialMap (K.orderedProd L)

Fixing a vertex b of the second factor gives the simplicial inclusion a ↦ (a, b) of the first factor into the ordered product.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.prodMkLeft K L b hb = { toFun := fun (a : α) => (a, b), map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_prodMkLeft {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (b : β) (hb : {b} ∈ L) : ⇑(prodMkLeft K L b hb) = fun (a : α) => (a, b)

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.prodMkLeft_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (b : β) (hb : {b} ∈ L) (a : α) : (prodMkLeft K L b hb) a = (a, b)

theorem PreAbstractSimplicialComplex.SimplicialMap.map_prodMkLeft_le_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (b : β) (hb : {b} ∈ L) : (K.map fun (a : α) => (a, b)) ≤ K.orderedProd L

The fixed-second-coordinate copy of the first factor is a subcomplex of the ordered product.

def PreAbstractSimplicialComplex.SimplicialMap.prodMkRight {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (a : α) (ha : {a} ∈ K) : L.SimplicialMap (K.orderedProd L)

Fixing a vertex a of the first factor gives the simplicial inclusion b ↦ (a, b) of the second factor into the ordered product.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.prodMkRight K L a ha = { toFun := fun (b : β) => (a, b), map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_prodMkRight {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (a : α) (ha : {a} ∈ K) : ⇑(prodMkRight K L a ha) = fun (b : β) => (a, b)

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.prodMkRight_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (a : α) (ha : {a} ∈ K) (b : β) : (prodMkRight K L a ha) b = (a, b)

theorem PreAbstractSimplicialComplex.SimplicialMap.map_prodMkRight_le_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) (a : α) (ha : {a} ∈ K) : (L.map fun (b : β) => (a, b)) ≤ K.orderedProd L

The fixed-first-coordinate copy of the second factor is a subcomplex of the ordered product.

def PreAbstractSimplicialComplex.SimplicialMap.orderedProdMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {Kγ : PreAbstractSimplicialComplex γ} {Lδ : PreAbstractSimplicialComplex δ} (f : K.SimplicialMap Kγ) (g : L.SimplicialMap Lδ) (hf : Monotone ⇑f) (hg : Monotone ⇑g) : (K.orderedProd L).SimplicialMap (Kγ.orderedProd Lδ)

Monotone simplicial maps induce a simplicial map between ordered products. Monotonicity is needed because the product triangulation depends on the chosen vertex orders.

Equations

• f.orderedProdMap g hf hg = { toFun := fun (p : α × β) => (f p.1, g p.2), map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_orderedProdMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {Kγ : PreAbstractSimplicialComplex γ} {Lδ : PreAbstractSimplicialComplex δ} (f : K.SimplicialMap Kγ) (g : L.SimplicialMap Lδ) (hf : Monotone ⇑f) (hg : Monotone ⇑g) : ⇑(f.orderedProdMap g hf hg) = fun (p : α × β) => (f p.1, g p.2)

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.orderedProdMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [LinearOrder α] [LinearOrder β] [LinearOrder γ] [LinearOrder δ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {Kγ : PreAbstractSimplicialComplex γ} {Lδ : PreAbstractSimplicialComplex δ} (f : K.SimplicialMap Kγ) (g : L.SimplicialMap Lδ) (hf : Monotone ⇑f) (hg : Monotone ⇑g) (p : α × β) : (f.orderedProdMap g hf hg) p = (f p.1, g p.2)

def AbstractSimplicialComplex.orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : AbstractSimplicialComplex α) (L : AbstractSimplicialComplex β) : AbstractSimplicialComplex (α × β)

The ordered product of two abstract simplicial complexes.

Equations

• K.orderedProd L = PreAbstractSimplicialComplex.toAbstractSimplicialComplex (α × β) (K.orderedProd L.toPreAbstractSimplicialComplex) ⋯

@[simp]

theorem AbstractSimplicialComplex.orderedProd_toPreAbstractSimplicialComplex {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} : (K.orderedProd L).toPreAbstractSimplicialComplex = K.orderedProd L.toPreAbstractSimplicialComplex

Forgetting that the ordered product contains every singleton recovers the product of the underlying precomplexes.

@[simp]

theorem AbstractSimplicialComplex.mem_orderedProd_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {σ : Finset (α × β)} : σ ∈ K.orderedProd L ↔ Finset.image Prod.fst σ ∈ K ∧ Finset.image Prod.snd σ ∈ L ∧ IsChain (fun (x1 x2 : α × β) => x1 ≤ x2) ↑σ

Membership in an abstract ordered product has the same projected-face and chain characterization as for precomplexes.

theorem AbstractSimplicialComplex.image_fst_mem_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : Finset.image Prod.fst σ ∈ K

The first-coordinate image of a face of an abstract ordered product is a face of the first factor.

theorem AbstractSimplicialComplex.image_snd_mem_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : Finset.image Prod.snd σ ∈ L

The second-coordinate image of a face of an abstract ordered product is a face of the second factor.

theorem AbstractSimplicialComplex.isChain_of_mem_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {σ : Finset (α × β)} (hσ : σ ∈ K.orderedProd L) : IsChain (fun (x1 x2 : α × β) => x1 ≤ x2) ↑σ

Every face of an abstract ordered product is a chain for the coordinatewise order.

theorem AbstractSimplicialComplex.orderedProd_mono {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K K' : AbstractSimplicialComplex α} {L L' : AbstractSimplicialComplex β} (hK : K ≤ K') (hL : L ≤ L') : K.orderedProd L ≤ K'.orderedProd L'

Ordered product is monotone in both abstract simplicial complexes.

def AbstractSimplicialComplex.orderedCylinder {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : AbstractSimplicialComplex (α × Fin 2)

The ordered simplicial cylinder on K, obtained by taking its ordered product with the standard one-simplex on Fin 2.

Equations

• K.orderedCylinder = K.orderedProd ⊤

@[simp]

theorem AbstractSimplicialComplex.orderedCylinder_toPreAbstractSimplicialComplex {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : K.orderedCylinder.toPreAbstractSimplicialComplex = K.orderedProd ⊤

The underlying precomplex of an ordered cylinder is the ordered product with the top precomplex on Fin 2.

@[simp]

theorem AbstractSimplicialComplex.mem_orderedCylinder_iff {α : Type u_1} [LinearOrder α] {K : AbstractSimplicialComplex α} {σ : Finset (α × Fin 2)} : σ ∈ K.orderedCylinder ↔ Finset.image Prod.fst σ ∈ K ∧ IsChain (fun (x1 x2 : α × Fin 2) => x1 ≤ x2) ↑σ

A face of the ordered cylinder is a face in the first coordinate and a chain in the product order. The second projection condition is automatic because the interval factor is top.

theorem AbstractSimplicialComplex.image_fst_mem_of_mem_orderedCylinder {α : Type u_1} [LinearOrder α] {K : AbstractSimplicialComplex α} {σ : Finset (α × Fin 2)} (hσ : σ ∈ K.orderedCylinder) : Finset.image Prod.fst σ ∈ K

The first-coordinate image of a face of an ordered cylinder is a face of the original complex.

theorem AbstractSimplicialComplex.isChain_of_mem_orderedCylinder {α : Type u_1} [LinearOrder α] {K : AbstractSimplicialComplex α} {σ : Finset (α × Fin 2)} (hσ : σ ∈ K.orderedCylinder) : IsChain (fun (x1 x2 : α × Fin 2) => x1 ≤ x2) ↑σ

Every face of an ordered cylinder is a chain for the product order.

theorem AbstractSimplicialComplex.finite_faces_orderedCylinder {α : Type u_1} [LinearOrder α] {K : AbstractSimplicialComplex α} (hfin : K.faces.Finite) : K.orderedCylinder.faces.Finite

The ordered cylinder of a finite abstract simplicial complex has finitely many faces.

theorem AbstractSimplicialComplex.isCone_orderedCylinder_of_isCone {α : Type u_1} [LinearOrder α] {K : AbstractSimplicialComplex α} {v : α} (hK : K.IsCone v) (hv : ∀ (w : α), {w} ∈ K → w ≤ v) : K.orderedCylinder.IsCone (v, 1)

The ordered cylinder of a cone whose apex bounds every vertex of the complex is a cone with apex the pair of that vertex and the terminal endpoint of the interval.

theorem AbstractSimplicialComplex.isCone_orderedCylinder_top {α : Type u_1} [LinearOrder α] [OrderTop α] : ⊤.orderedCylinder.IsCone (⊤, 1)

The ordered cylinder of the full abstract simplex is a cone with apex the greatest vertex at the terminal endpoint of the interval.

theorem AbstractSimplicialComplex.map_prodMk_zero_le_orderedCylinder {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : (K.map fun (a : α) => (a, 0)) ≤ K.orderedCylinder.toPreAbstractSimplicialComplex

The zero-end copy of a complex is a simplicial subcomplex of its ordered cylinder.

theorem AbstractSimplicialComplex.map_prodMk_one_le_orderedCylinder {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : (K.map fun (a : α) => (a, 1)) ≤ K.orderedCylinder.toPreAbstractSimplicialComplex

The one-end copy of a complex is a simplicial subcomplex of its ordered cylinder.

def AbstractSimplicialComplex.orderedCylinderZero {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : K.SimplicialMap K.orderedCylinder.toPreAbstractSimplicialComplex

The bundled simplicial inclusion of the zero endpoint into an ordered cylinder.

Equations

• K.orderedCylinderZero = PreAbstractSimplicialComplex.SimplicialMap.ofMapLE (fun (a : α) => (a, 0)) ⋯

@[simp]

theorem AbstractSimplicialComplex.coe_orderedCylinderZero {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : ⇑K.orderedCylinderZero = fun (a : α) => (a, 0)

@[simp]

theorem AbstractSimplicialComplex.orderedCylinderZero_apply {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) (a : α) : K.orderedCylinderZero a = (a, 0)

def AbstractSimplicialComplex.orderedCylinderOne {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : K.SimplicialMap K.orderedCylinder.toPreAbstractSimplicialComplex

The bundled simplicial inclusion of the one endpoint into an ordered cylinder.

Equations

• K.orderedCylinderOne = PreAbstractSimplicialComplex.SimplicialMap.ofMapLE (fun (a : α) => (a, 1)) ⋯

@[simp]

theorem AbstractSimplicialComplex.coe_orderedCylinderOne {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) : ⇑K.orderedCylinderOne = fun (a : α) => (a, 1)

@[simp]

theorem AbstractSimplicialComplex.orderedCylinderOne_apply {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) (a : α) : K.orderedCylinderOne a = (a, 1)

The following three computations pin down the staircase convention on the square. The two monotone triangles are faces, while the pair of incomparable off-diagonal vertices is not.

theorem AbstractSimplicialComplex.fstLeSndTriangle_mem_orderedProd_finTwo : {(0, 0), (0, 1), (1, 1)} ∈ ⊤.orderedProd ⊤

The fst ≤ snd triangle is a face of the ordered square.

theorem AbstractSimplicialComplex.sndLeFstTriangle_mem_orderedProd_finTwo : {(0, 0), (1, 0), (1, 1)} ∈ ⊤.orderedProd ⊤

The snd ≤ fst triangle is a face of the ordered square.

theorem AbstractSimplicialComplex.offDiagonalPair_notMem_orderedProd_finTwo : {(0, 1), (1, 0)} ∉ ⊤.orderedProd ⊤

The incomparable off-diagonal vertices do not form a face of the ordered square.