fix(algebraic_topology): added FQNs to simplicial locale (#6838)

This fix, which fully qualifies some notation, makes it so that
```
import algebraic_topology.simplicial_set
open_locale simplicial
```
works without errors.

src/algebraic_topology/simplicial_object.lean

@@ -38,7 +38,7 @@ namespace simplicial_object
 
 localized
   "notation X `_[`:1000 n `]` :=
-    (X : simplicial_object _).obj (opposite.op (simplex_category.mk n))"
+    (X : category_theory.simplicial_object _).obj (opposite.op (simplex_category.mk n))"
   in simplicial
 
 instance {J : Type v} [small_category J] [has_limits_of_shape J C] :

src/algebraic_topology/simplicial_set.lean

@@ -17,7 +17,7 @@ homotopy type theory.)
 
 We define the standard simplices `Δ[n]` as simplicial sets,
 and their boundaries `∂Δ[n]` and horns `Λ[n, i]`.
-(The notations are available via `open_locale sSet`.)
+(The notations are available via `open_locale simplicial`.)
 
 ## Future work
 
@@ -45,7 +45,7 @@ namespace sSet
 is the Yoneda embedding of `n`. -/
 def standard_simplex : simplex_category ⥤ sSet := yoneda
 
-localized "notation `Δ[`n`]` := standard_simplex.obj (simplex_category.mk n)" in simplicial
+localized "notation `Δ[`n`]` := sSet.standard_simplex.obj (simplex_category.mk n)" in simplicial
 
 instance : inhabited sSet := ⟨Δ[0]⟩
 
@@ -65,7 +65,7 @@ def boundary (n : ℕ) : sSet :=
   map := λ m₁ m₂ f α, ⟨f.unop ≫ (α : Δ[n].obj m₁),
   by { intro h, apply α.property, exact function.surjective.of_comp h }⟩ }
 
-localized "notation `∂Δ[`n`]` := boundary n" in simplicial
+localized "notation `∂Δ[`n`]` := sSet.boundary n" in simplicial
 
 /-- The inclusion of the boundary of the `n`-th standard simplex into that standard simplex. -/
 def boundary_inclusion (n : ℕ) :
@@ -88,7 +88,7 @@ def horn (n : ℕ) (i : fin (n+1)) : sSet :=
     exact set.range_comp_subset_range _ _ hj,
   end⟩ }
 
-localized "notation `Λ[`n`, `i`]` := horn (n : ℕ) i" in simplicial
+localized "notation `Λ[`n`, `i`]` := sSet.horn (n : ℕ) i" in simplicial
 
 /-- The inclusion of the `i`-th horn of the `n`-th standard simplex into that standard simplex. -/
 def horn_inclusion (n : ℕ) (i : fin (n+1)) :