Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

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 #

source
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.

Instances
    source
    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)
    source
    theorem SSet.Nonsingular.of_mono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] [Y.Nonsingular] :
    X.Nonsingular

    Kerodon Tag 02MK

    source
    theorem SSet.Nonsingular.of_iso {X Y : SSet} (e : X ≅ Y) [X.Nonsingular] :
    Y.Nonsingular
    source
    instance SSet.instNonsingularToSSet {X : SSet} (A : X.Subcomplex) [X.Nonsingular] :
    A.toSSet.Nonsingular
    source
    instance SSet.instNonsingularNerve (T : Type u_1) [PartialOrder T] :
    (CategoryTheory.nerve T).Nonsingular

    Kerodon Tag 02MT

    source
    instance SSet.instNonsingularObjSimplexCategoryStdSimplex (n : SimplexCategory) :
    (stdSimplex.obj n).Nonsingular
    source
    instance SSet.instNonsingularTensorObjObjSimplexCategoryStdSimplex (n m : SimplexCategory) :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj n) (stdSimplex.obj m)).Nonsingular
    source
    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

    source
    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