Nonempty simplicial sets

@[reducible, inline]

abbrev SSet.Nonempty (X : SSet) : Prop

A simplicial set is nonempty when the type of 0-simplices is nonempty.

Equations

• X.Nonempty = Nonempty (X.obj (Opposite.op { len := 0 }))

instance SSet.instNonemptyObjOppositeSimplexCategoryOfNonempty (X : SSet) (n : SimplexCategoryᵒᵖ) [X.Nonempty] : Nonempty (X.obj n)

instance SSet.instNonemptyNOfNonempty (X : SSet) [X.Nonempty] : Nonempty X.N

instance SSet.instNonemptySOfNonempty (X : SSet) [X.Nonempty] : Nonempty X.S

instance SSet.instNonemptyNerveOfNonempty (T : Type u) [Preorder T] [Nonempty T] : (CategoryTheory.nerve T).Nonempty

instance SSet.instNonemptyObjSimplexCategoryStdSimplex (n : SimplexCategory) : (stdSimplex.obj n).Nonempty

theorem SSet.nonempty_of_hom {X Y : SSet} (f : Y ⟶ X) [Y.Nonempty] : X.Nonempty

theorem SSet.notNonempty_iff_hasDimensionLT_zero (X : SSet) : ¬X.Nonempty ↔ X.HasDimensionLT 0

def SSet.isInitialOfNotNonempty {X : SSet} (hX : ¬X.Nonempty) : CategoryTheory.Limits.IsInitial X

If a simplicial set is not nonempty, it is an initial object.

Equations

• SSet.isInitialOfNotNonempty hX = CategoryTheory.Limits.IsInitial.ofUniqueHom (fun (x : SSet) => { app := fun (x_1 : SimplexCategoryᵒᵖ) (x_2 : X.obj x_1) => isEmptyElim x_2, naturality := ⋯ }) ⋯