Nonsingular simplicial sets

In this file, we introduce a typeclass SSet.Nonsingular for a simplicial set X : SSet: it says that for any non-degenerate simplex x : X _⦋n⦌, the corresponding morphism Δ[n] ⟶ X is a monomorphism. This notion is useful in the context of the study of the subdivision functor (TODO @joelriou).

The condition SSet.Nonsingular is a weaker condition compared to the notion of "polyhedral complex" which appears in the article Simplicial approximation by Jardine, and which says that there exists a monomorphism X ⟶ nerve T where T is a partially ordered type.

References

• Vegard Fjellbo and John Rognes, Exponentials of non-singular simplicial sets
• J. F. Jardine, Simplicial approximation

class SSet.Nonsingular (X : SSet) : Prop

A simplicial set X is nonsingular if for any nondegenerate simplex x (of dimension n), the corresponding morphism Δ[n] ⟶ X is a monomorphism.

• mono {n : ℕ} (x : ↑(X.nonDegenerate n)) : CategoryTheory.Mono (yonedaEquiv.symm ↑x)

theorem SSet.Nonsingular.mono' {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) : CategoryTheory.Mono (yonedaEquiv.symm x)

theorem SSet.Nonsingular.of_mono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] [Y.Nonsingular] : X.Nonsingular

Kerodon Tag 02MK

theorem SSet.Nonsingular.of_iso {X Y : SSet} (e : X ≅ Y) [X.Nonsingular] : Y.Nonsingular

instance SSet.instNonsingularToSSet {X : SSet} (A : X.Subcomplex) [X.Nonsingular] : A.toSSet.Nonsingular

instance SSet.instNonsingularNerve (T : Type u_1) [PartialOrder T] : (CategoryTheory.nerve T).Nonsingular

Kerodon Tag 02MT

instance SSet.instNonsingularObjSimplexCategoryStdSimplex (n : SimplexCategory) : (stdSimplex.obj n).Nonsingular

instance SSet.instNonsingularTensorObjObjSimplexCategoryStdSimplex (n m : SimplexCategory) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj n) (stdSimplex.obj m)).Nonsingular

theorem SSet.nonDegenerate_δ {X : SSet} [X.Nonsingular] {n : ℕ} {x : X.obj (Opposite.op { len := n + 1 })} (hx : x ∈ X.nonDegenerate (n + 1)) (i : Fin (n + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Kerodon Tag 02MH

theorem SSet.Nonsingular.δ_injective {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) (hx : x ∈ X.nonDegenerate (n + 1)) (i j : Fin (n + 2)) (hij : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) x) : i = j

theorem SSet.Nonsingular.injective_map {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) {m : SimplexCategory} {f g : m ⟶ { len := n }} (h : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (X.map g.op)) x) : f = g

theorem SSet.Nonsingular.isIso_toOfSimplex {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) : CategoryTheory.IsIso (Subcomplex.toOfSimplex x)

noncomputable def SSet.Nonsingular.iso {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) : stdSimplex.obj { len := n } ≅ (Subcomplex.ofSimplex x).toSSet

If x : X _⦋n⦌ is a nondegenerate simplex of a nonsingular simplcial set, this is the isomorphism Δ[n] ≅ Subcomplex.ofSimplex x induced by x.

Equations

• SSet.Nonsingular.iso x hx = CategoryTheory.asIso (SSet.Subcomplex.toOfSimplex x)

@[simp]

theorem SSet.Nonsingular.iso_hom {X : SSet} [X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n) : (iso x hx).hom = Subcomplex.toOfSimplex x

theorem SSet.N.existsUnique_of_le {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : ∃! f : { len := x.dim } ⟶ { len := y.dim }, CategoryTheory.Mono f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

noncomputable def SSet.N.monoOfLE {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : { len := x.dim } ⟶ { len := y.dim }

Given an inequality x ≤ y between nondegenerate simplices of a nonsingular simplicial set X, this is the corresponding morphism ⦋x.dim⦌ ⟶ ⦋y.dim⦌ in the simplex category.

Equations

• SSet.N.monoOfLE h = ⋯.choose

instance SSet.N.instMonoSimplexCategoryMonoOfLE {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : CategoryTheory.Mono (monoOfLE h)

@[simp]

theorem SSet.N.map_monoOfLE {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : (CategoryTheory.ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex

@[simp]

theorem SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : CategoryTheory.CategoryStruct.comp (stdSimplex.map (monoOfLE h)) (yonedaEquiv.symm y.simplex) = yonedaEquiv.symm x.simplex

theorem SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex_assoc {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) {Z : SSet} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.map (monoOfLE h)) (CategoryTheory.CategoryStruct.comp (yonedaEquiv.symm y.simplex) h✝) = CategoryTheory.CategoryStruct.comp (yonedaEquiv.symm x.simplex) h✝

theorem SSet.N.monoOfLE_eq_iff {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) (g : { len := x.dim } ⟶ { len := y.dim }) [CategoryTheory.Mono g] : monoOfLE h = g ↔ (CategoryTheory.ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex

@[simp]

theorem SSet.N.monoOfLE_refl {X : SSet} [X.Nonsingular] (x : X.N) : monoOfLE ⋯ = CategoryTheory.CategoryStruct.id { len := x.dim }

@[simp]

theorem SSet.N.monoOfLE_comp {X : SSet} [X.Nonsingular] {x y z : X.N} (h : x ≤ y) (h' : y ≤ z) : CategoryTheory.CategoryStruct.comp (monoOfLE h) (monoOfLE h') = monoOfLE ⋯

@[simp]

theorem SSet.N.monoOfLE_comp_assoc {X : SSet} [X.Nonsingular] {x y z : X.N} (h : x ≤ y) (h' : y ≤ z) {Z : SimplexCategory} (h✝ : { len := z.dim } ⟶ Z) : CategoryTheory.CategoryStruct.comp (monoOfLE h) (CategoryTheory.CategoryStruct.comp (monoOfLE h') h✝) = CategoryTheory.CategoryStruct.comp (monoOfLE ⋯) h✝