Maps of abstract simplicial complexes

This file bundles simplicial maps between pre-abstract simplicial complexes. A simplicial map is a map of ambient vertex types which sends every face to a face. The file supplies the identity, composition, restriction to subcomplexes, and extension to a larger complex, together with the connection to Mathlib's image complex PreAbstractSimplicialComplex.map.

These maps are basic infrastructure for subdivision and geometric realization in the geometric topology roadmap. We work with PreAbstractSimplicialComplex, since constructions such as links and elementary collapses naturally change the set of vertices represented by singleton faces.

structure PreAbstractSimplicialComplex.SimplicialMap {α : Type u_1} {β : Type u_2} [DecidableEq β] (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : Type (max u_1 u_2)

A simplicial map between pre-abstract simplicial complexes is a map of their ambient vertex types which sends faces to faces.

• toFun : α → β

  The map on the ambient vertex types.

• map_face' ⦃σ : Finset α⦄ : σ ∈ K → Finset.image self.toFun σ ∈ L

  The image of every face is a face.

theorem PreAbstractSimplicialComplex.SimplicialMap.ext_iff {α : Type u_1} {β : Type u_2} {inst✝ : DecidableEq β} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {x y : K.SimplicialMap L} : x = y ↔ x.toFun = y.toFun

theorem PreAbstractSimplicialComplex.SimplicialMap.ext {α : Type u_1} {β : Type u_2} {inst✝ : DecidableEq β} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {x y : K.SimplicialMap L} (toFun : x.toFun = y.toFun) : x = y

@[instance_reducible]

instance PreAbstractSimplicialComplex.SimplicialMap.instFunLike {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} : FunLike (K.SimplicialMap L) α β

Equations

• PreAbstractSimplicialComplex.SimplicialMap.instFunLike = { coe := PreAbstractSimplicialComplex.SimplicialMap.toFun, coe_injective := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_mk {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : α → β) (hf : ∀ ⦃σ : Finset α⦄, σ ∈ K → Finset.image f σ ∈ L) : ⇑{ toFun := f, map_face' := hf } = f

theorem PreAbstractSimplicialComplex.SimplicialMap.map_face {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) {σ : Finset α} (hσ : σ ∈ K) : Finset.image (⇑f) σ ∈ L

A simplicial map sends a face to a face.

theorem PreAbstractSimplicialComplex.SimplicialMap.map_le_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : α → β) : K.map f ≤ L ↔ ∀ ⦃σ : Finset α⦄, σ ∈ K → Finset.image f σ ∈ L

A vertex map is simplicial exactly when its image complex is a subcomplex of the codomain.

def PreAbstractSimplicialComplex.SimplicialMap.ofMapLE {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : α → β) (h : K.map f ≤ L) : K.SimplicialMap L

Construct a simplicial map from containment of the image complex in the codomain.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.ofMapLE f h = { toFun := f, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_ofMapLE {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : α → β) (h : K.map f ≤ L) : ⇑(ofMapLE f h) = f

theorem PreAbstractSimplicialComplex.SimplicialMap.map_le {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) : K.map ⇑f ≤ L

The image complex of a simplicial map is contained in its codomain.

def PreAbstractSimplicialComplex.SimplicialMap.id {α : Type u_1} [DecidableEq α] (K : PreAbstractSimplicialComplex α) : K.SimplicialMap K

The identity simplicial map.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.id K = { toFun := id, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_id {α : Type u_1} {K : PreAbstractSimplicialComplex α} [DecidableEq α] : ⇑(id K) = _root_.id

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.id_apply {α : Type u_1} {K : PreAbstractSimplicialComplex α} [DecidableEq α] (x : α) : (id K) x = x

def PreAbstractSimplicialComplex.SimplicialMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {P : PreAbstractSimplicialComplex γ} (g : L.SimplicialMap P) (f : K.SimplicialMap L) : K.SimplicialMap P

Composition of simplicial maps.

Equations

• g.comp f = { toFun := ⇑g ∘ ⇑f, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {P : PreAbstractSimplicialComplex γ} (g : L.SimplicialMap P) (f : K.SimplicialMap L) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {P : PreAbstractSimplicialComplex γ} (g : L.SimplicialMap P) (f : K.SimplicialMap L) (x : α) : (g.comp f) x = g (f x)

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.comp_id {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq α] (f : K.SimplicialMap L) : f.comp (id K) = f

Composing a simplicial map on the right with the identity leaves it unchanged.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.id_comp {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) : (id L).comp f = f

Composing a simplicial map on the left with the identity leaves it unchanged.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq β] [DecidableEq γ] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {P : PreAbstractSimplicialComplex γ} {P' : PreAbstractSimplicialComplex δ} [DecidableEq δ] (h : P.SimplicialMap P') (g : L.SimplicialMap P) (f : K.SimplicialMap L) : (h.comp g).comp f = h.comp (g.comp f)

Composition of simplicial maps is associative.

def PreAbstractSimplicialComplex.SimplicialMap.domainRestrict {α : Type u_1} {β : Type u_2} [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) (h : K' ≤ K) : K'.SimplicialMap L

Restrict the domain of a simplicial map to a subcomplex.

Equations

• f.domainRestrict h = { toFun := ⇑f, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_domainRestrict {α : Type u_1} {β : Type u_2} [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) (h : K' ≤ K) : ⇑(f.domainRestrict h) = ⇑f

def PreAbstractSimplicialComplex.SimplicialMap.codomainExtend {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) (h : L ≤ L') : K.SimplicialMap L'

Regard a simplicial map as landing in a larger complex.

Equations

• f.codomainExtend h = { toFun := ⇑f, map_face' := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_codomainExtend {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (f : K.SimplicialMap L) (h : L ≤ L') : ⇑(f.codomainExtend h) = ⇑f

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

Every vertex map is simplicial into its image complex.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.toImage K f = PreAbstractSimplicialComplex.SimplicialMap.ofMapLE f ⋯

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_toImage {α : Type u_1} {β : Type u_2} [DecidableEq β] (K : PreAbstractSimplicialComplex α) (f : α → β) : ⇑(toImage K f) = f

def PreAbstractSimplicialComplex.SimplicialMap.inclusion {α : Type u_1} {K K' : PreAbstractSimplicialComplex α} [DecidableEq α] (h : K ≤ K') : K.SimplicialMap K'

The inclusion of a subcomplex, acting as the identity on the ambient vertex type.

Equations

• PreAbstractSimplicialComplex.SimplicialMap.inclusion h = (PreAbstractSimplicialComplex.SimplicialMap.id K).codomainExtend h

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.coe_inclusion {α : Type u_1} {K K' : PreAbstractSimplicialComplex α} [DecidableEq α] (h : K ≤ K') : ⇑(inclusion h) = _root_.id

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.inclusion_apply {α : Type u_1} {K K' : PreAbstractSimplicialComplex α} [DecidableEq α] (h : K ≤ K') (x : α) : (inclusion h) x = x

def TauCeti.PreAbstractSimplicialComplex.SimplicialMap.faceOrderHom {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) : SetLike.Face K →o SetLike.Face L

A simplicial map induces a monotone map between face posets by taking the image of every face.

Equations

• TauCeti.PreAbstractSimplicialComplex.SimplicialMap.faceOrderHom f = { toFun := fun (σ : TauCeti.SetLike.Face K) => ⟨Finset.image ⇑f ↑σ, ⋯⟩, monotone' := ⋯ }

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.coe_faceOrderHom_apply {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) (σ : SetLike.Face K) : ↑((faceOrderHom f) σ) = Finset.image ⇑f ↑σ

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.faceOrderHom_id {α : Type u_1} {K : PreAbstractSimplicialComplex α} [DecidableEq α] : faceOrderHom (PreAbstractSimplicialComplex.SimplicialMap.id K) = OrderHom.id

Mapping face posets along the identity is the identity order homomorphism.

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.faceOrderHom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {M : PreAbstractSimplicialComplex γ} [DecidableEq β] [DecidableEq γ] (g : L.SimplicialMap M) (f : K.SimplicialMap L) : faceOrderHom (g.comp f) = (faceOrderHom g).comp (faceOrderHom f)

Mapping face posets along a composite is composition of the face-poset maps.