English
If the underlying quiver of a category C is thin (at most one morphism between any two objects), then each n-simplex in the nerve is determined by its 0-skeleton; in particular, two simplices with the same underlying object are equal.
Русский
Если орнаментующий граф (кварь) категории C тонкий (между любыми двумя объектами существует не более одной морфизмы), то каждый n-симплекс в нерве определяется своей нулевой оболочкой; если два симплекса имеют одинаковый базовый объект, они равны.
LaTeX
$$$\text{If } \text{IsThin}(C)\text{ then } \forall n, x,y \in (\mathrm{nerve}\,C)_n,\; x\!\!\!\!\! = y\text{ whenever } x.{obj}=y.{obj}.$$$
Lean4
@[ext]
theorem ext_of_isThin [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ} {x y : (nerve C).obj n} (h : x.obj = y.obj) : x = y :=
ComposableArrows.ext (by simp [h]) (by subsingleton)
