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.

TODO

• show that X.skeleton (n + 1) is obtained from X.skeleton n by attaching ∂Δ[n] ⟶ Δ[n] cells (this also holds for skeletonOfMono i) (@joelriou).
• 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.

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

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

theorem SSet.ofSimplex_le_skeleton (X : SSet) {i : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk 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 (SimplexCategory.mk 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) [CategoryTheory.Mono i] : ℕ →o Y.Subcomplex

The skeleton of a monomorphism i : X ⟶ Y of simplicial sets. It sends n : ℕ to Subcomplex.range i ⊔ Y.skeleton n.

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

@[simp]

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

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

theorem SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] {d : ℕ} (x : ↑(Y.nonDegenerate d)) (n : ℕ) : ↑x ∈ ((skeletonOfMono i) n).obj (Opposite.op (SimplexCategory.mk d)) ↔ ↑x ∈ Set.range (i.app (Opposite.op (SimplexCategory.mk d))) ∨ d < n

theorem SSet.skeletonOfMono_obj_eq_top {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] {d n : ℕ} (h : d < n) : ((skeletonOfMono i) n).obj (Opposite.op (SimplexCategory.mk d)) = ⊤

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