style: use simplex notation (⦋n⦌) where possible (#25322)

`StandardSimplex.mk n` is replaced with `⦋n⦌` where possible (except in notation and macros, which are left untouched). This includes opening `Simplicial` (`scoped`) in two files. Also, outdated and unused `local notation` `[n]` for `StandardSimplex.mk n` is removed.



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: thorimur

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -30,9 +30,9 @@ object, when `C` has finite products. We call this `cechNerveTerminalFrom`. When
 -/
 
 
-open CategoryTheory
+open CategoryTheory Limits
 
-open CategoryTheory.Limits
+open scoped Simplicial
 
 noncomputable section
 
@@ -107,7 +107,7 @@ def equivalenceRightToLeft (X : SimplicialObject.Augmented C) (F : Arrow C)
   right := G.right
   w := by
     have := G.w
-    apply_fun fun e => e.app (Opposite.op <| SimplexCategory.mk 0) at this
+    apply_fun fun e => e.app (Opposite.op ⦋0⦌) at this
     simpa using this
 
 /-- A helper function used in defining the Čech adjunction. -/
@@ -228,12 +228,12 @@ def augmentedCechConerve : Arrow C ⥤ CosimplicialObject.Augmented C where
 def equivalenceLeftToRight (F : Arrow C) (X : CosimplicialObject.Augmented C)
     (G : F.augmentedCechConerve ⟶ X) : F ⟶ Augmented.toArrow.obj X where
   left := G.left
-  right := (WidePushout.ι _ 0 ≫ G.right.app (SimplexCategory.mk 0) :)
+  right := (WidePushout.ι _ 0 ≫ G.right.app ⦋0⦌ :)
   w := by
     dsimp
     rw [@WidePushout.arrow_ι_assoc _ _ _ _ _ (fun (_ : Fin 1) => F.hom)
       (by dsimp; infer_instance)]
-    exact congr_app G.w (SimplexCategory.mk 0)
+    exact congr_app G.w ⦋0⦌
 
 /-- A helper function used in defining the Čech conerve adjunction. -/
 @[simps!]
@@ -247,7 +247,7 @@ def equivalenceRightToLeft (F : Arrow C) (X : CosimplicialObject.Augmented C)
           (by
             rintro j
             rw [← Arrow.w_assoc G]
-            have t := X.hom.naturality (SimplexCategory.const (SimplexCategory.mk 0) x j)
+            have t := X.hom.naturality (SimplexCategory.const ⦋0⦌ x j)
             dsimp at t ⊢
             simp only [Category.id_comp] at t
             rw [← t])
@@ -298,7 +298,7 @@ abbrev cechConerveAdjunction : augmentedCechConerve ⊣ (Augmented.toArrow : _ 
 
 end CosimplicialObject
 
-/-- Given an object `X : C`, the natural simplicial object sending `[n]` to `Xⁿ⁺¹`. -/
+/-- Given an object `X : C`, the natural simplicial object sending `⦋n⦌` to `Xⁿ⁺¹`. -/
 def cechNerveTerminalFrom {C : Type u} [Category.{v} C] [HasFiniteProducts C] (X : C) :
     SimplicialObject C where
   obj n := ∏ᶜ fun _ : Fin (n.unop.len + 1) => X

Mathlib/AlgebraicTopology/MooreComplex.lean

@@ -37,6 +37,8 @@ open CategoryTheory CategoryTheory.Limits
 
 open Opposite
 
+open scoped Simplicial
+
 namespace AlgebraicTopology
 
 variable {C : Type*} [Category C] [Abelian C]
@@ -55,7 +57,7 @@ variable (X : SimplicialObject C)
 
 /-- The normalized Moore complex in degree `n`, as a subobject of `X n`.
 -/
-def objX : ∀ n : ℕ, Subobject (X.obj (op (SimplexCategory.mk n)))
+def objX : ∀ n : ℕ, Subobject (X.obj (op ⦋n⦌))
   | 0 => ⊤
   | n + 1 => Finset.univ.inf fun k : Fin (n + 1) => kernelSubobject (X.δ k.succ)
 
@@ -117,7 +119,7 @@ variable {X} {Y : SimplicialObject C} (f : X ⟶ Y)
 @[simps!]
 def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
   ChainComplex.ofHom _ _ _ _ _ _
-    (fun n => factorThru _ (arrow _ ≫ f.app (op (SimplexCategory.mk n))) (by
+    (fun n => factorThru _ (arrow _ ≫ f.app (op ⦋n⦌)) (by
       cases n <;> dsimp
       · apply top_factors
       · refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

@@ -568,7 +568,7 @@ instance : skeletalFunctor.Faithful where
 
 instance : skeletalFunctor.EssSurj where
   mem_essImage X :=
-    ⟨mk (Fintype.card X - 1 : ℕ),
+    ⟨⦋(Fintype.card X - 1 : ℕ)⦌,
       ⟨by
         have aux : Fintype.card X = Fintype.card X - 1 + 1 :=
           (Nat.succ_pred_eq_of_pos <| Fintype.card_pos_iff.mpr ⟨⊥⟩).symm
@@ -732,9 +732,9 @@ theorem iso_eq_iso_refl {x : SimplexCategory} (e : x ≅ x) : e = Iso.refl x :=
 theorem eq_id_of_isIso {x : SimplexCategory} (f : x ⟶ x) [IsIso f] : f = 𝟙 _ :=
   congr_arg (fun φ : _ ≅ _ => φ.hom) (iso_eq_iso_refl (asIso f))
 
-theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk (n + 1) ⟶ Δ')
+theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : ⦋n + 1⦌ ⟶ Δ')
     (i : Fin (n + 1)) (hi : θ.toOrderHom (Fin.castSucc i) = θ.toOrderHom i.succ) :
-    ∃ θ' : mk n ⟶ Δ', θ = σ i ≫ θ' := by
+    ∃ θ' : ⦋n⦌ ⟶ Δ', θ = σ i ≫ θ' := by
   use δ i.succ ≫ θ
   ext x : 3
   simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
@@ -763,9 +763,9 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
         Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
       omega
 
-theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (n + 1) ⟶ Δ')
+theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : ⦋n + 1⦌ ⟶ Δ')
     (hθ : ¬Function.Injective θ.toOrderHom) :
-    ∃ (i : Fin (n + 1)) (θ' : mk n ⟶ Δ'), θ = σ i ≫ θ' := by
+    ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ' := by
   simp only [Function.Injective, exists_prop, not_forall] at hθ
   -- as θ is not injective, there exists `x<y` such that `θ x = θ y`
   -- and then, `θ x = θ (x+1)`
@@ -783,8 +783,8 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
   · rw [Fin.castSucc_castPred, h₁]
     exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)
 
-theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
-    (i : Fin (n + 2)) (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ mk n, θ = θ' ≫ δ i := by
+theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ ⦋n + 1⦌)
+    (i : Fin (n + 2)) (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ ⦋n⦌, θ = θ' ≫ δ i := by
   use θ ≫ σ (.predAbove (.last n) i)
   ext x : 3
   suffices ∀ j ≠ i, i.succAbove (((Fin.last n).predAbove i).predAbove j) = j by
@@ -793,9 +793,9 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
   intro j hj
   cases i using Fin.lastCases <;> simp [hj]
 
-theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
+theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ ⦋n + 1⦌)
     (hθ : ¬Function.Surjective θ.toOrderHom) :
-    ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ mk n), θ = θ' ≫ δ i := by
+    ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i := by
   obtain ⟨i, hi⟩ := not_forall.mp hθ
   use i
   exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)
@@ -817,7 +817,7 @@ theorem eq_id_of_epi {x : SimplexCategory} (i : x ⟶ x) [Epi i] : i = 𝟙 _ :=
     eq_self_iff_true, and_true]
   infer_instance
 
-theorem eq_σ_of_epi {n : ℕ} (θ : mk (n + 1) ⟶ mk n) [Epi θ] : ∃ i : Fin (n + 1), θ = σ i := by
+theorem eq_σ_of_epi {n : ℕ} (θ : ⦋n + 1⦌ ⟶ ⦋n⦌) [Epi θ] : ∃ i : Fin (n + 1), θ = σ i := by
   rcases eq_σ_comp_of_not_injective θ (by
     by_contra h
     simpa using le_of_mono (mono_iff_injective.mpr h)) with ⟨i, θ', h⟩
@@ -828,7 +828,7 @@ theorem eq_σ_of_epi {n : ℕ} (θ : mk (n + 1) ⟶ mk n) [Epi θ] : ∃ i : Fin
   haveI := CategoryTheory.epi_of_epi (σ i) θ'
   rw [h, eq_id_of_epi θ', Category.comp_id]
 
-theorem eq_δ_of_mono {n : ℕ} (θ : mk n ⟶ mk (n + 1)) [Mono θ] : ∃ i : Fin (n + 2), θ = δ i := by
+theorem eq_δ_of_mono {n : ℕ} (θ : ⦋n⦌ ⟶ ⦋n + 1⦌) [Mono θ] : ∃ i : Fin (n + 2), θ = δ i := by
   rcases eq_comp_δ_of_not_surjective θ (by
     by_contra h
     simpa using le_of_epi (epi_iff_surjective.mpr h)) with ⟨i, θ', h⟩

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -438,9 +438,9 @@ def toArrow : Augmented C ⥤ Arrow C where
 /-- The compatibility of a morphism with the augmentation, on 0-simplices -/
 @[reassoc]
 theorem w₀ {X Y : Augmented C} (f : X ⟶ Y) :
-    (Augmented.drop.map f).app (op (SimplexCategory.mk 0)) ≫ Y.hom.app (op (SimplexCategory.mk 0)) =
-      X.hom.app (op (SimplexCategory.mk 0)) ≫ Augmented.point.map f := by
-  convert congr_app f.w (op (SimplexCategory.mk 0))
+    (Augmented.drop.map f).app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌) =
+      X.hom.app (op ⦋0⦌) ≫ Augmented.point.map f := by
+  convert congr_app f.w (op ⦋0⦌)
 
 variable (C)
 
@@ -663,12 +663,12 @@ theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
 
 @[reassoc (attr := simp)]
 theorem δ_naturality {X' X : CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) :
-    X.δ i ≫ f.app (SimplexCategory.mk (n + 1)) = f.app (SimplexCategory.mk n) ≫ X'.δ i :=
+    X.δ i ≫ f.app ⦋n + 1⦌ = f.app ⦋n⦌ ≫ X'.δ i :=
   f.naturality _
 
 @[reassoc (attr := simp)]
 theorem σ_naturality {X' X : CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 1)) :
-    X.σ i ≫ f.app (SimplexCategory.mk n) = f.app (SimplexCategory.mk (n + 1)) ≫ X'.σ i :=
+    X.σ i ≫ f.app ⦋n⦌ = f.app ⦋n + 1⦌ ≫ X'.σ i :=
   f.naturality _
 
 variable (C)

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -179,7 +179,7 @@ noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) :
   fac s j := by
     ext x
     obtain ⟨⟨i, hi⟩, ⟨f :  _ ⟶ _⟩, rfl⟩ := j.mk_surjective
-    obtain ⟨i, rfl⟩ : ∃ j, SimplexCategory.mk j = i := ⟨_, i.mk_len⟩
+    obtain ⟨i, rfl⟩ : ∃ j, ⦋j⦌ = i := ⟨_, i.mk_len⟩
     dsimp at hi ⊢
     apply sx.spineInjective
     dsimp

Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

@@ -76,8 +76,6 @@ def nerve₂Adj.counit : nerveFunctor₂ ⋙ hoFunctor₂.{u} ⟶ 𝟭 Cat where
   app _ := nerve₂Adj.counit.app _
   naturality _ _ _ := nerve₂Adj.counit.naturality _
 
-local notation (priority := high) "[" n "]" => SimplexCategory.mk n
-
 variable {C : Type u} [SmallCategory C] {X : SSet.Truncated.{u} 2}
     (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C)
 

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -25,9 +25,9 @@ open CategoryTheory Limits Simplicial Opposite
 
 namespace SSet
 
-/-- The functor `SimplexCategory ⥤ SSet` which sends `SimplexCategory.mk n` to
-the standard simplex `Δ[n]` is a cosimplicial object in the category of simplicial sets.
-(This functor is essentially given by the Yoneda embedding). -/
+/-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the standard simplex `Δ[n]` is a
+cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
+Yoneda embedding). -/
 def stdSimplex : CosimplicialObject SSet.{u} :=
   yoneda ⋙ uliftFunctor
 
@@ -67,7 +67,7 @@ lemma ext {n d : ℕ} (x y : Δ[n] _⦋d⦌) (h : ∀ (i : Fin (d + 1)), x i = y
 
 @[simp]
 lemma objEquiv_toOrderHom_apply {n i : ℕ}
-    (x : (stdSimplex.{u} ^⦋n⦌).obj (op (.mk i))) (j : Fin (i + 1)) :
+    (x : (stdSimplex.{u} ^⦋n⦌).obj (op ⦋i⦌)) (j : Fin (i + 1)) :
     DFunLike.coe (F := Fin (i + 1) →o Fin (n + 1))
       ((DFunLike.coe (F := Δ[n].obj (op ⦋i⦌) ≃ (⦋i⦌ ⟶ ⦋n⦌))
         objEquiv x)).toOrderHom j = x j :=
@@ -79,8 +79,7 @@ lemma objEquiv_symm_comp {n n' : SimplexCategory} {m : SimplexCategoryᵒᵖ}
       (stdSimplex.map g).app _ (objEquiv.{u}.symm f) := rfl
 
 @[simp]
-lemma objEquiv_symm_apply {n m : ℕ}
-    (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)) :
+lemma objEquiv_symm_apply {n m : ℕ} (f : ⦋m⦌ ⟶ ⦋n⦌) (i : Fin (m + 1)) :
     (objEquiv.{u}.symm f : Δ[n] _⦋m⦌) i = f.toOrderHom i := rfl
 
 /-- Constructor for simplices of the standard simplex which takes a `OrderHom` as an input. -/
@@ -91,7 +90,7 @@ abbrev objMk {n : SimplexCategory} {m : SimplexCategoryᵒᵖ}
 
 @[simp]
 lemma objMk_apply {n m : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) (i : Fin (m + 1)) :
-    objMk.{u} (n := .mk n) (m := op (.mk m)) f i = f i :=
+    objMk.{u} (n := ⦋n⦌) (m := op ⦋m⦌) f i = f i :=
   rfl
 
 /-- The `m`-simplices of the `n`-th standard simplex are
@@ -231,7 +230,7 @@ then the face `face S` of `Δ[n]` is representable by `m`,
 i.e. `face S` is isomorphic to `Δ[m]`, see `stdSimplex.isoOfRepresentableBy`. -/
 def faceRepresentableBy {n : ℕ} (S : Finset (Fin (n + 1)))
     (m : ℕ) (e : Fin (m + 1) ≃o S) :
-    (face S : SSet.{u}).RepresentableBy (.mk m) where
+    (face S : SSet.{u}).RepresentableBy ⦋m⦌ where
   homEquiv {j} :=
     { toFun f := ⟨objMk ((OrderHom.Subtype.val S.toSet).comp
           (e.toOrderEmbedding.toOrderHom.comp f.toOrderHom)), fun _ ↦ by aesop⟩
@@ -251,9 +250,9 @@ def faceRepresentableBy {n : ℕ} (S : Finset (Fin (n + 1)))
           (e.apply_symm_apply ⟨(objEquiv x).toOrderHom i, _⟩) }
   homEquiv_comp f g := by aesop
 
-/-- If a simplicial set `X` is representable by `SimplexCategory.mk m` for some `m : ℕ`,
-then this is the corresponding isomorphism `Δ[m] ≅ X`. -/
-def isoOfRepresentableBy {X : SSet.{u}} {m : ℕ} (h : X.RepresentableBy (.mk m)) :
+/-- If a simplicial set `X` is representable by `⦋m⦌` for some `m : ℕ`, then this is the
+corresponding isomorphism `Δ[m] ≅ X`. -/
+def isoOfRepresentableBy {X : SSet.{u}} {m : ℕ} (h : X.RepresentableBy ⦋m⦌) :
     Δ[m] ≅ X :=
   NatIso.ofComponents (fun n ↦ Equiv.toIso (objEquiv.trans h.homEquiv)) (by
     intros