Structures · Topology
SSet.Nonsingular
A simplicial set X is nonsingular if for any
nondegenerate simplex x (of dimension n), the corresponding
morphism Δ[n] ⟶ X is a monomorphism.
- Shape
- One type argument · adds mono
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every SSet.Nonsingular is also a
Concrete types that are instances4
- CategoryTheory.Functor.obj
- CategoryTheory.MonoidalCategoryStruct.tensorObj
- SSet.Subcomplex.toSSet
- CategoryTheory.nerve
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- SSet.N.monoOfLE
- SSet.Nonsingular.mono'
- SSet.N.map_monoOfLE
- SSet.N.toSemiSimplexCategory
- SSet.functorN'
- SSet.N.existsUnique_of_le
- SSet.Nonsingular.iso
- SSet.coconeN'
- SSet.N.monoOfLE_comp
- SSet.Nonsingular.injective_map
- SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex
- SSet.Nonsingular.of_mono
- SSet.coconeN'_pt
- SSet.Subcomplex.PairingCore.instIsProperOfNonsingular
- SSet.N.monoOfLE_refl
- SSet.Nonsingular.isIso_toOfSimplex
- SSet.Nonsingular.iso_hom
- SSet.Nonsingular.of_iso
- SSet.nonDegenerate_δ
- SSet.N.instMonoSimplexCategoryMonoOfLE
- SSet.isColimitCoconeN'
- SSet.instNonsingularToSSet
- SSet.N.monoOfLE_comp_assoc
- SSet.N.toSemiSimplexCategory_map
- SSet.Nonsingular.δ_injective
- SSet.N.monoOfLE.congr_simp
- SSet.Nonsingular.iso.congr_simp
- SSet.functorN'Iso
- SSet.Nonsingular.mono
- SSet.coconeN'_ι_app
- SSet.N.monoOfLE_eq_iff
- SSet.N.toSemiSimplexCategory_obj
- SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex_assoc