doc: fix typos in SimplicialSet docstrings (leanprover-community#41571)

This PR fixes four docstring typos in `Mathlib/AlgebraicTopology/SimplicialSet/`: "simplcial" → "simplicial" in `Nonsingular.iso`, the broken code reference `s : X : N` → `s : X.N` (plus a missing final period) in `N.toSemiSimplexCategory`, a stray trailing semicolon in `stdSimplex.fullyFaithful`, and "the colimit of the its monogenous subcomplexes" → "the colimit of its monogenous subcomplexes" in `isColimitCoconeN`.

Follow-up to [leanprover-community#40254 (feat(AlgebraicTopology): nonsingular simplicial set is colimit of standard simplices)](leanprover-community#40254).

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesColimit.lean

@@ -89,7 +89,7 @@ lemma fac (s : Cocone X.functorN) (x : X.N) :
 end isColimitCoconeN
 
 open isColimitCoconeN in
-/-- If `X : SSet`, then `X` is the colimit of the its monogenous subcomplexes.
+/-- If `X : SSet`, then `X` is the colimit of its monogenous subcomplexes.
 (Note: a monogenous subcomplex of `X` is generated by a unique nondegenerate
 simplex `x : X.N`.) -/
 public noncomputable def isColimitCoconeN : IsColimit X.coconeN where

Mathlib/AlgebraicTopology/SimplicialSet/Nonsingular.lean

@@ -121,7 +121,7 @@ lemma Nonsingular.isIso_toOfSimplex [X.Nonsingular]
   rw [Subcomplex.isIso_toOfSimplex_iff]
   exact Nonsingular.mono' x hx
 
-/-- If `x : X _⦋n⦌` is a nondegenerate simplex of a nonsingular simplcial set,
+/-- If `x : X _⦋n⦌` is a nondegenerate simplex of a nonsingular simplicial set,
 this is the isomorphism `Δ[n] ≅ Subcomplex.ofSimplex x` induced by `x`. -/
 @[expose, simps! hom]
 noncomputable def Nonsingular.iso

Mathlib/AlgebraicTopology/SimplicialSet/NonsingularColimit.lean

@@ -37,7 +37,7 @@ namespace N
 set_option backward.isDefEq.respectTransparency false in
 /-- If `X` is a nonsingular simplicial set, this is the functor
 `X.N ⥤ SemiSimplexCategory` which sends a nondegenerate
-simplex `s : X : N` to `⦋s.dim⦌ₛ` -/
+simplex `s : X.N` to `⦋s.dim⦌ₛ`. -/
 @[simps obj map]
 noncomputable def toSemiSimplexCategory : X.N ⥤ SemiSimplexCategory where
   obj s := ⦋s.dim⦌ₛ

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -51,7 +51,7 @@ namespace stdSimplex
 
 open Finset Opposite SimplexCategory
 
-/-- The functor `stdSimplex : SimplexCategory ⥤ SSet` is fully faithful; -/
+/-- The functor `stdSimplex : SimplexCategory ⥤ SSet` is fully faithful. -/
 abbrev fullyFaithful : stdSimplex.{u}.FullyFaithful :=
   ULiftYoneda.fullyFaithful SimplexCategory