The skeleton of a simplicial set

In this file, we define the skeleton X.skeleton : ℕ →o X.Subcomplex of a simplicial set X. For any n : ℕ, X.skeleton n is the subcomplex of X that is generated by (non-degenerate) simplices of dimension < n.

If i : X ⟶ Y is a monomorphism, we define skeletonOfMono i : ℕ →o Y.Subcomplex so that skeletonOfMono i n = Subcomplex.range i ⊔ Y.skeleton n. We show that this filtration is part of a relative cell complex structure for i, with basic cells given by boundary inclusions ∂Δ[d] ⟶ Δ[d] for all nondegenerate d-simplices of Y which do not belong to the range of i.

TODO

• show that (SSet.sk n).obj X is isomorphic to X.skeleton (n + 1)

def SSet.skeleton (X : SSet) : ℕ →o X.Subcomplex

X.skeleton n is the subcomplex of X generated by (non-degenerate) simplices of dimension < n.

Equations

• X.skeleton = { toFun := fun (n : ℕ) => ⨆ (i : Fin n), ⨆ (x : ↑(X.nonDegenerate ↑i)), SSet.Subcomplex.ofSimplex ↑x, monotone' := ⋯ }

theorem SSet.mem_skeleton (X : SSet) {i : ℕ} (x : X.obj (Opposite.op { len := i })) {n : ℕ} (hi : i < n := by lia) : x ∈ (X.skeleton n).obj (Opposite.op { len := i })

theorem SSet.skeleton_obj_eq_top (X : SSet) {d n : ℕ} (h : d < n) : (X.skeleton n).obj (Opposite.op { len := d }) = ⊤

theorem SSet.ofSimplex_le_skeleton (X : SSet) {i : ℕ} (x : X.obj (Opposite.op { len := i })) {n : ℕ} (hi : i < n) : Subcomplex.ofSimplex x ≤ X.skeleton n

theorem SSet.mem_skeleton_obj_iff_of_nonDegenerate (X : SSet) {d : ℕ} (x : ↑(X.nonDegenerate d)) (n : ℕ) : ↑x ∈ (X.skeleton n).obj (Opposite.op { len := d }) ↔ d < n

@[simp]

theorem SSet.skeleton_zero (X : SSet) : X.skeleton 0 = ⊥

theorem SSet.iSup_skeleton (X : SSet) : ⨆ (n : ℕ), X.skeleton n = ⊤

theorem SSet.skeleton_succ (X : SSet) (n : ℕ) : X.skeleton (n + 1) = X.skeleton n ⊔ ⨆ (x : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑x

def SSet.skeletonOfMono {X Y : SSet} (i : X ⟶ Y) : ℕ →o Y.Subcomplex

The skeleton of a monomorphism i : X ⟶ Y of simplicial sets. It sends n : ℕ to Subcomplex.range i ⊔ Y.skeleton n. See SSet.relativeCellComplexOfMono for the main result regarding this definition. (Even though [Mono i] is technically not required in this definition, the intended use of this definition and the corresponding API is when [Mono i] holds.)

Equations

• SSet.skeletonOfMono i = { toFun := fun (n : ℕ) => SSet.Subcomplex.range i ⊔ Y.skeleton n, monotone' := ⋯ }

theorem SSet.skeleton_le_skeletonOfMono {X Y : SSet} (i : X ⟶ Y) (n : ℕ) : Y.skeleton n ≤ (skeletonOfMono i) n

@[simp]

theorem SSet.skeletonOfMono_zero {X Y : SSet} (i : X ⟶ Y) : (skeletonOfMono i) 0 = Subcomplex.range i

theorem SSet.iSup_skeletonOfMono {X Y : SSet} (i : X ⟶ Y) : ⨆ (n : ℕ), (skeletonOfMono i) n = ⊤

theorem SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate {X Y : SSet} (i : X ⟶ Y) {d : ℕ} (x : ↑(Y.nonDegenerate d)) (n : ℕ) : ↑x ∈ ((skeletonOfMono i) n).obj (Opposite.op { len := d }) ↔ ↑x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) ∨ d < n

theorem SSet.skeletonOfMono_obj_eq_top {X Y : SSet} (i : X ⟶ Y) {d n : ℕ} (h : d < n) : ((skeletonOfMono i) n).obj (Opposite.op { len := d }) = ⊤

theorem SSet.skeletonOfMono_succ {X Y : SSet} (i : X ⟶ Y) (n : ℕ) : (skeletonOfMono i) (n + 1) = (skeletonOfMono i) n ⊔ ⨆ (x : ↑(Y.nonDegenerate n)), ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (Opposite.op { len := n })), Subcomplex.ofSimplex ↑x

The main next technical result is that if i : X ⟶ Y is a monomorphism of simplicial sets and d : ℕ, there is a pushout square:

                                t i d
∐ fun (c : Cell i d) ↦ ∂Δ[d] ----------> skeletonOfMono i d
               |                                   |
         l i d |                                   | r i d
               v                b i d              v
∐ fun (c : Cell i d) ↦ Δ[d]  ----------> skeletonOfMono i (d + 1)

The index type Cell i d identifies to the type of nondegenerate d-simplices of Y not in the range of i.

structure SSet.relativeCellComplexOfMono.Cell {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : Type u

If i : X ⟶ Y is a monomorphism of simplicial sets and d : ℕ, this is the type of nondegenerate d-simplices of Y which do not belong to the range of i.

• simplex : Y.obj (Opposite.op { len := d })

  a d-simplex in the target of the monomorphism

• nonDegenerate : self.simplex ∈ Y.nonDegenerate d
• notMem : self.simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))

theorem SSet.relativeCellComplexOfMono.Cell.ext_iff {X Y : SSet} {i : X ⟶ Y} {d : ℕ} {x y : Cell i d} : x = y ↔ x.simplex = y.simplex

theorem SSet.relativeCellComplexOfMono.Cell.ext {X Y : SSet} {i : X ⟶ Y} {d : ℕ} {x y : Cell i d} (simplex : x.simplex = y.simplex) : x = y

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.sigmaStdSimplex {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : SSet

If i : X ⟶ Y is a monomorphism of simplicial sets and d : ℕ, this is a coproduct of copies of Δ[d] indexed by the nondegenerate d-simplices of Y not in the range of i.

Equations

• SSet.relativeCellComplexOfMono.sigmaStdSimplex i d = ∐ fun (x : SSet.relativeCellComplexOfMono.Cell i d) => SSet.stdSimplex.obj { len := d }

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.sigmaBoundary {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : SSet

If i : X ⟶ Y is a monomorphism of simplicial sets and d : ℕ, this is a coproduct of copies of ∂Δ[d] indexed by the nondegenerate d-simplices of Y not in the range of i.

Equations

• SSet.relativeCellComplexOfMono.sigmaBoundary i d = ∐ fun (x : SSet.relativeCellComplexOfMono.Cell i d) => (SSet.boundary d).toSSet

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.Cell.ιSigmaStdSimplex {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : stdSimplex.obj { len := d } ⟶ sigmaStdSimplex i d

Given a monomorphism i : X ⟶ Y of simplicial sets and a nondegenerate d-simplex of Y not in the range of i, this is the inclusion of the corresponding summand of the coproduct sigmaStdSimplex i d.

Equations

• c.ιSigmaStdSimplex = CategoryTheory.Limits.Sigma.ι (fun (x : SSet.relativeCellComplexOfMono.Cell i d) => SSet.stdSimplex.obj { len := d }) c

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.Cell.ιSigmaBoundary {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : (boundary d).toSSet ⟶ sigmaBoundary i d

Given a monomorphism i : X ⟶ Y of simplicial sets and a nondegenerate d-simplex of Y not in the range of i, this is the inclusion of the corresponding summand of the coproduct sigmaBoundary i d.

Equations

• c.ιSigmaBoundary = CategoryTheory.Limits.Sigma.ι (fun (x : SSet.relativeCellComplexOfMono.Cell i d) => (SSet.boundary d).toSSet) c

@[reducible, inline]

abbrev SSet.relativeCellComplexOfMono.Cell.map {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : stdSimplex.obj { len := d } ⟶ Y

Given a monomorphism i : X ⟶ Y of simplicial sets and a nondegenerate d-simplex of Y not in the range of i, this is the corresponding morphism Δ[d] ⟶ Y.

Equations

• c.map = SSet.yonedaEquiv.symm c.simplex

theorem SSet.relativeCellComplexOfMono.Cell.mem_skeletonOfMono_obj_iff {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) {d' : ℕ} : c.simplex ∈ ((skeletonOfMono i) d').obj (Opposite.op { len := d }) ↔ c.simplex ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) ∨ d < d'

theorem SSet.relativeCellComplexOfMono.Cell.range_map_le {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : Subcomplex.range c.map ≤ (skeletonOfMono i) (d + 1)

@[simp]

theorem SSet.relativeCellComplexOfMono.Cell.preimage_map {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : ((skeletonOfMono i) d).preimage c.map = boundary d

theorem SSet.relativeCellComplexOfMono.ιSigmaStdSimplex_jointly_surjective {X Y : SSet} {i : X ⟶ Y} {d n : ℕ} (a : (sigmaStdSimplex i d).obj (Opposite.op { len := n })) : ∃ (c : Cell i d) (x : (stdSimplex.obj { len := d }).obj (Opposite.op { len := n })), (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := n }))) x = a

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.l {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : sigmaBoundary i d ⟶ sigmaStdSimplex i d

the left morphism of the pushout square isPushout i d: this is the coproduct of copies of the boundary inclusion ∂Δ[d] ⟶ Δ[d] indexed by the nondegenerate d-simplices of Y not in the range of i.

Equations

• SSet.relativeCellComplexOfMono.l i d = CategoryTheory.Limits.Sigma.map fun (x : SSet.relativeCellComplexOfMono.Cell i d) => (SSet.boundary d).ι

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.t {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : sigmaBoundary i d ⟶ ((skeletonOfMono i) d).toSSet

the top morphism of the pushout square isPushout i d.

Equations

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

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplexOfMono.b {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : sigmaStdSimplex i d ⟶ ((skeletonOfMono i) (d + 1)).toSSet

the bottom morphism of the pushout square isPushout i d.

Equations

• SSet.relativeCellComplexOfMono.b i d = CategoryTheory.Limits.Sigma.desc fun (c : SSet.relativeCellComplexOfMono.Cell i d) => SSet.Subcomplex.lift c.map ⋯

@[reducible, inline]

abbrev SSet.relativeCellComplexOfMono.r {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : ((skeletonOfMono i) d).toSSet ⟶ ((skeletonOfMono i) (d + 1)).toSSet

the right morphism of the pushout square isPushout i d.

Equations

• SSet.relativeCellComplexOfMono.r i d = SSet.Subcomplex.homOfLE ⋯

theorem SSet.relativeCellComplexOfMono.w {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : CategoryTheory.CategoryStruct.comp (t i d) (r i d) = CategoryTheory.CategoryStruct.comp (l i d) (b i d)

theorem SSet.relativeCellComplexOfMono.w_assoc {X Y : SSet} (i : X ⟶ Y) (d : ℕ) {Z : SSet} (h : ((skeletonOfMono i) (d + 1)).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (t i d) (CategoryTheory.CategoryStruct.comp (r i d) h) = CategoryTheory.CategoryStruct.comp (l i d) (CategoryTheory.CategoryStruct.comp (b i d) h)

theorem SSet.relativeCellComplexOfMono.Cell.ι_t_ι_eq_ι_l_b_ι {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary (CategoryTheory.CategoryStruct.comp (t i d) ((skeletonOfMono i) d).ι) = CategoryTheory.CategoryStruct.comp (boundary d).ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (b i d) ((skeletonOfMono i) (d + 1)).ι))

theorem SSet.relativeCellComplexOfMono.Cell.ι_t_ι_eq_ι_l_b_ι_assoc {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary (CategoryTheory.CategoryStruct.comp (t i d) (CategoryTheory.CategoryStruct.comp ((skeletonOfMono i) d).ι h)) = CategoryTheory.CategoryStruct.comp (boundary d).ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (b i d) (CategoryTheory.CategoryStruct.comp ((skeletonOfMono i) (d + 1)).ι h)))

theorem SSet.relativeCellComplexOfMono.Cell.ι_l {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary (l i d) = CategoryTheory.CategoryStruct.comp (boundary d).ι c.ιSigmaStdSimplex

theorem SSet.relativeCellComplexOfMono.Cell.ι_l_assoc {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) {Z : SSet} (h : sigmaStdSimplex i d ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary (CategoryTheory.CategoryStruct.comp (l i d) h) = CategoryTheory.CategoryStruct.comp (boundary d).ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex h)

@[simp]

theorem SSet.relativeCellComplexOfMono.Cell.ι_b_ι {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) : CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (b i d) ((skeletonOfMono i) (d + 1)).ι) = c.map

@[simp]

theorem SSet.relativeCellComplexOfMono.Cell.ι_b_ι_assoc {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (b i d) (CategoryTheory.CategoryStruct.comp ((skeletonOfMono i) (d + 1)).ι h)) = CategoryTheory.CategoryStruct.comp c.map h

theorem SSet.relativeCellComplexOfMono.Cell.b_app_ι_app_objEquiv_symm_val {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : Cell i d) {n : SimplexCategory} (f : n ⟶ { len := d }) : ↑((CategoryTheory.ConcreteCategory.hom ((b i d).app (Opposite.op n))) ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op n))) (stdSimplex.objEquiv.symm f))) = (CategoryTheory.ConcreteCategory.hom (Y.map f.op)) c.simplex

theorem SSet.relativeCellComplexOfMono.isPullback {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : CategoryTheory.IsPullback (t i d) (l i d) (r i d) (b i d)

theorem SSet.relativeCellComplexOfMono.sup_range_r_range_b {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d) = ⊤

theorem SSet.relativeCellComplexOfMono.range_r_app_union_range_b_app {X Y : SSet} (i : X ⟶ Y) (d : ℕ) (n : SimplexCategoryᵒᵖ) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((r i d).app n)) ∪ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((b i d).app n)) = Set.univ

theorem SSet.relativeCellComplexOfMono.isPushout_aux {X Y : SSet} {i : X ⟶ Y} {d n : ℕ} (y : (sigmaStdSimplex i d).obj (Opposite.op { len := n })) (hy : y ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((l i d).app (Opposite.op { len := n })))) : ∃ (c : Cell i d) (f : { len := n } ⟶ { len := d }) (_ : CategoryTheory.Epi f), (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := n }))) (stdSimplex.objEquiv.symm f) = y

theorem SSet.relativeCellComplexOfMono.isPushout {X Y : SSet} (i : X ⟶ Y) (d : ℕ) : CategoryTheory.IsPushout (t i d) (l i d) (r i d) (b i d)

noncomputable def SSet.relativeCellComplexOfMono {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : HomotopicalAlgebra.RelativeCellComplex (fun (n : ℕ) (x : Unit) => (boundary n).ι) i

If i : X ⟶ Y is a monomorphism of simplicial sets, then it is a relative cell complex with basic cells given by boundary inclusions ∂Δ[d] ⟶ Δ[d], one for each nondegenerate d-simplex of Y not in the range of X.

Equations

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

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_g₁ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).g₁ = relativeCellComplexOfMono.t i d

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_m {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).m = relativeCellComplexOfMono.l i d

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_isColimit₂ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).isColimit₂ = CategoryTheory.Limits.coproductIsCoproduct fun (i : relativeCellComplexOfMono.Cell i d) => stdSimplex.obj { len := d }

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_cofan₂ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).cofan₂ = CategoryTheory.Limits.Cofan.mk (∐ fun (i : relativeCellComplexOfMono.Cell i d) => stdSimplex.obj { len := d }) (CategoryTheory.Limits.Sigma.ι fun (i : relativeCellComplexOfMono.Cell i d) => stdSimplex.obj { len := d })

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_g₂ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).g₂ = relativeCellComplexOfMono.b i d

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_cofan₁ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).cofan₁ = CategoryTheory.Limits.Cofan.mk (∐ fun (i : relativeCellComplexOfMono.Cell i d) => (boundary d).toSSet) (CategoryTheory.Limits.Sigma.ι fun (i : relativeCellComplexOfMono.Cell i d) => (boundary d).toSSet)

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_π {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) (x✝¹ : relativeCellComplexOfMono.Cell i d) : ((relativeCellComplexOfMono i).attachCells d x✝).π x✝¹ = ()

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_isColimit₁ {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).isColimit₁ = CategoryTheory.Limits.coproductIsCoproduct fun (i : relativeCellComplexOfMono.Cell i d) => (boundary d).toSSet

@[simp]

theorem SSet.relativeCellComplexOfMono_incl_app {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (x✝ : ℕ) : (relativeCellComplexOfMono i).incl.app x✝ = (⋯.functor.obj x✝).ι

@[simp]

theorem SSet.relativeCellComplexOfMono_isoBot {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : (relativeCellComplexOfMono i).isoBot = Subcomplex.eqToIso ⋯ ≪≫ (CategoryTheory.asIso (Subcomplex.toRange i)).symm

@[simp]

theorem SSet.relativeCellComplexOfMono_F {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : (relativeCellComplexOfMono i).F = ⋯.functor.comp Subcomplex.toSSetFunctor

@[simp]

theorem SSet.relativeCellComplexOfMono_isColimit {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : (relativeCellComplexOfMono i).isColimit = (CategoryTheory.Limits.isColimitOfPreserves Subcomplex.toSSetFunctor (CategoryTheory.Limits.CompleteLattice.colimitCocone ⋯.functor).isColimit).ofIsoColimit (CategoryTheory.Limits.Cocone.ext (Subcomplex.eqToIso ⋯ ≪≫ Subcomplex.topIso Y) ⋯)

@[simp]

theorem SSet.relativeCellComplexOfMono_attachCells_ι {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((relativeCellComplexOfMono i).attachCells d x✝).ι = relativeCellComplexOfMono.Cell i d

@[reducible, inline]

noncomputable abbrev SSet.relativeCellComplex (X : SSet) : HomotopicalAlgebra.RelativeCellComplex (fun (n : ℕ) (x : Unit) => (boundary n).ι) ⊥.ι

If X is a simplicial set, then the inclusion (⊥ : SSet) ⟶ X of the empty subcomplex of X is a relative cell complex with basic cells given by boundary inclusions ∂Δ[d] ⟶ Δ[d], one for each nondegenerate d-simplex of X.

Equations

• X.relativeCellComplex = SSet.relativeCellComplexOfMono ⊥.ι

def SSet.relativeCellComplexCellsEquiv {X : SSet} : X.relativeCellComplex.Cells ≃ X.N

The bijection between the cells of relativeCellComplex X and the type X.N of nondegenerate simplices of the simplicial set X.

Equations

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

@[simp]

theorem SSet.relativeCellComplexCellsEquiv_symm_apply_j {X : SSet} (s : X.N) : (relativeCellComplexCellsEquiv.symm s).j = s.dim

@[simp]

theorem SSet.relativeCellComplexCellsEquiv_apply {X : SSet} (c : X.relativeCellComplex.Cells) : relativeCellComplexCellsEquiv c = N.mk c.k.simplex ⋯

@[simp]

theorem SSet.relativeCellComplexCellsEquiv_symm_apply_k_simplex {X : SSet} (s : X.N) : (relativeCellComplexCellsEquiv.symm s).k.simplex = s.simplex