Documentation

TauCeti.AlgebraicTopology.SimplicialComplex.Subdivision.Basic

Barycentric subdivision of abstract simplicial complexes #

The vertices of the first barycentric subdivision of a simplicial complex K are its faces, which are always nonempty: PreAbstractSimplicialComplex requires its face collection to be a lower set relative to Finset.Nonempty, so the empty face never occurs. A collection of these new vertices spans a face exactly when the corresponding faces of K form a chain under inclusion. Equivalently, the barycentric subdivision is the order complex of the face poset.

The construction is made for PreAbstractSimplicialComplex, since links, deletions, and collapse subcomplexes need not contain every ambient singleton. Its result is an AbstractSimplicialComplex: every face of the original complex is genuinely a vertex of the subdivision. Simplicial maps act on face posets by taking vertexwise images, yielding the functorial map barycentricSubdivisionMap.

This supplies the subdivision primitive required by Layer 11 of the GeometricTopology roadmap before combinatorial spheres and balls can be defined up to subdivision. The definition follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2, "Derived Subdivisions". Identifying the realizations of a complex and its subdivision is separate geometric realization work. The functoriality here is only at the level of abstract complexes: the canonical identification of a subdivision's realization with the original realization is not natural in arbitrary simplicial maps.

Main definitions #

Main results #

source
noncomputable def TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision {α : Type u_1} (K : PreAbstractSimplicialComplex α) :
AbstractSimplicialComplex (SetLike.Face K)

The first barycentric subdivision of K: its vertices are the faces of K, and its faces are the nonempty finite chains of faces under inclusion.

Equations
Instances For
    source
    theorem TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision_eq_orderComplex {α : Type u_1} (K : PreAbstractSimplicialComplex α) :
    barycentricSubdivision K = AbstractSimplicialComplex.orderComplex (SetLike.Face K)

    Barycentric subdivision is the order complex of the face poset.

    source
    @[simp]
    theorem TauCeti.PreAbstractSimplicialComplex.mem_barycentricSubdivision_iff {α : Type u_1} {K : PreAbstractSimplicialComplex α} {τ : Finset (SetLike.Face K)} :
    τ ∈ barycentricSubdivision K ↔ τ.Nonempty ∧ IsChain (fun (x1 x2 : SetLike.Face K) => x1 ≤ x2) ↑τ

    A collection of faces of K is a face of its barycentric subdivision exactly when it is nonempty and totally ordered by inclusion.

    source
    theorem TauCeti.PreAbstractSimplicialComplex.mem_barycentricSubdivision_iff' {α : Type u_1} {K : PreAbstractSimplicialComplex α} {ρ : Finset (SetLike.Face K)} :
    ρ ∈ barycentricSubdivision K ↔ ρ.Nonempty ∧ ∀ σ ∈ ρ, ∀ τ ∈ ρ, ↑σ ⊆ ↑τ ∨ ↑τ ⊆ ↑σ

    A collection is a face of the barycentric subdivision exactly when it is nonempty and every two original faces in the collection are nested.

    source
    theorem TauCeti.PreAbstractSimplicialComplex.pair_mem_barycentricSubdivision_iff {α : Type u_1} {K : PreAbstractSimplicialComplex α} [DecidableEq α] (σ τ : SetLike.Face K) :
    {σ, τ} ∈ barycentricSubdivision K ↔ ↑σ ⊆ ↑τ ∨ ↑τ ⊆ ↑σ

    Two faces of K span an edge in its barycentric subdivision exactly when one is contained in the other.

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

    source
    theorem TauCeti.PreAbstractSimplicialComplex.subset_or_subset_of_mem_barycentricSubdivision {α : Type u_1} {K : PreAbstractSimplicialComplex α} {ρ : Finset (SetLike.Face K)} (hρ : ρ ∈ barycentricSubdivision K) {σ τ : SetLike.Face K} (hσ : σ ∈ ρ) (hτ : τ ∈ ρ) :
    ↑σ ⊆ ↑τ ∨ ↑τ ⊆ ↑σ

    Every two original faces occurring in one face of the barycentric subdivision are nested.

    source
    def TauCeti.PreAbstractSimplicialComplex.SimplicialMap.barycentricSubdivisionMap {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) :
    (barycentricSubdivision K).SimplicialMap (barycentricSubdivision L).toPreAbstractSimplicialComplex

    A simplicial map induces a simplicial map between barycentric subdivisions by mapping every face-vertex to its vertexwise image.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.barycentricSubdivisionMap_eq_orderComplexMap {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) :
      barycentricSubdivisionMap f = AbstractSimplicialComplex.orderComplexMap (faceOrderHom f)

      The subdivision map is the order-complex map induced by the map on face posets.

      source
      theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.coe_barycentricSubdivisionMap {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) :
      ⇑(barycentricSubdivisionMap f) = ⇑(faceOrderHom f)
      source
      @[simp]
      theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.coe_barycentricSubdivisionMap_apply {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq β] (f : K.SimplicialMap L) (σ : SetLike.Face K) :
      ↑((barycentricSubdivisionMap f) σ) = Finset.image ⇑f ↑σ
      source
      @[simp]
      theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.barycentricSubdivisionMap_id {α : Type u_1} {K : PreAbstractSimplicialComplex α} [DecidableEq α] :
      barycentricSubdivisionMap (PreAbstractSimplicialComplex.SimplicialMap.id K) = PreAbstractSimplicialComplex.SimplicialMap.id (barycentricSubdivision K).toPreAbstractSimplicialComplex

      Barycentric subdivision sends the identity simplicial map to the identity simplicial map.

      source
      @[simp]
      theorem TauCeti.PreAbstractSimplicialComplex.SimplicialMap.barycentricSubdivisionMap_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) :
      barycentricSubdivisionMap (g.comp f) = (barycentricSubdivisionMap g).comp (barycentricSubdivisionMap f)

      Barycentric subdivision sends a composite of simplicial maps to the composite of their induced maps.