feat(AlgebraicTopology): notation ⦋n⦌ for SimplexCategory.mk n (#21565)

We change the notation for `SimplexCategory.mk n` from `[n]` (which conflicts with the `List` notation) to `⦋n⦌`. This also allows removing many type annotations of the form `(⦋n⦌ : SimplexCategory)`. This was done in commit [`ceb03e9`](ceb03e9).

[Zulip poll](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simplex.20category.20notations/near/497502272)

Author: gio256

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -135,7 +135,7 @@ variable {X} {Y}
 
 /-- The alternating face map complex, on morphisms -/
 def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
-  ChainComplex.ofHom _ _ _ _ _ _ (fun n => f.app (op [n])) fun n => by
+  ChainComplex.ofHom _ _ _ _ _ _ (fun n => f.app (op ⦋n⦌)) fun n => by
     dsimp
     rw [comp_sum, sum_comp]
     refine Finset.sum_congr rfl fun _ _ => ?_
@@ -145,7 +145,7 @@ def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
     apply f.naturality
 
 @[simp]
-theorem map_f (f : X ⟶ Y) (n : ℕ) : (map f).f n = f.app (op [n]) :=
+theorem map_f (f : X ⟶ Y) (n : ℕ) : (map f).f n = f.app (op ⦋n⦌) :=
   rfl
 
 end AlternatingFaceMapComplex
@@ -172,7 +172,7 @@ theorem alternatingFaceMapComplex_obj_d (X : SimplicialObject C) (n : ℕ) :
 
 @[simp]
 theorem alternatingFaceMapComplex_map_f {X Y : SimplicialObject C} (f : X ⟶ Y) (n : ℕ) :
-    ((alternatingFaceMapComplex C).map f).f n = f.app (op [n]) :=
+    ((alternatingFaceMapComplex C).map f).f n = f.app (op ⦋n⦌) :=
   rfl
 
 theorem map_alternatingFaceMapComplex {D : Type*} [Category D] [Preadditive D] (F : C ⥤ D)
@@ -198,7 +198,7 @@ theorem map_alternatingFaceMapComplex {D : Type*} [Category D] [Preadditive D] (
 
 theorem karoubi_alternatingFaceMapComplex_d (P : Karoubi (SimplicialObject C)) (n : ℕ) :
     ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
-      P.p.app (op [n + 1]) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n := by
+      P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n := by
   dsimp
   simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
     Karoubi.zsmul_hom, Preadditive.comp_zsmul]
@@ -221,7 +221,7 @@ def ε [Limits.HasZeroObject C] :
       SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C where
   app X := by
     refine (ChainComplex.toSingle₀Equiv _ _).symm ?_
-    refine ⟨X.hom.app (op [0]), ?_⟩
+    refine ⟨X.hom.app (op ⦋0⦌), ?_⟩
     dsimp
     rw [alternatingFaceMapComplex_obj_d, objD, Fin.sum_univ_two, Fin.val_zero,
       pow_zero, one_smul, Fin.val_one, pow_one, neg_smul, one_smul, add_comp,
@@ -237,7 +237,7 @@ def ε [Limits.HasZeroObject C] :
 
 @[simp]
 lemma ε_app_f_zero [Limits.HasZeroObject C] (X : SimplicialObject.Augmented C) :
-    (ε.app X).f 0 = X.hom.app (op [0]) :=
+    (ε.app X).f 0 = X.hom.app (op ⦋0⦌) :=
   ChainComplex.toSingle₀Equiv_symm_apply_f_zero _ _
 
 @[simp]
@@ -296,7 +296,7 @@ variable (X Y : CosimplicialObject C)
 /-- The differential on the alternating coface map complex is the alternate
 sum of the coface maps -/
 @[simp]
-def objD (n : ℕ) : X.obj [n] ⟶ X.obj [n + 1] :=
+def objD (n : ℕ) : X.obj ⦋n⦌ ⟶ X.obj ⦋n + 1⦌ :=
   ∑ i : Fin (n + 2), (-1 : ℤ) ^ (i : ℕ) • X.δ i
 
 theorem d_eq_unop_d (n : ℕ) :
@@ -311,14 +311,14 @@ theorem d_squared (n : ℕ) : objD X n ≫ objD X (n + 1) = 0 := by
 
 /-- The alternating coface map complex, on objects -/
 def obj : CochainComplex C ℕ :=
-  CochainComplex.of (fun n => X.obj [n]) (objD X) (d_squared X)
+  CochainComplex.of (fun n => X.obj ⦋n⦌) (objD X) (d_squared X)
 
 variable {X} {Y}
 
 /-- The alternating face map complex, on morphisms -/
 @[simp]
 def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
-  CochainComplex.ofHom _ _ _ _ _ _ (fun n => f.app [n]) fun n => by
+  CochainComplex.ofHom _ _ _ _ _ _ (fun n => f.app ⦋n⦌) fun n => by
     dsimp
     rw [comp_sum, sum_comp]
     refine Finset.sum_congr rfl fun x _ => ?_

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -397,7 +397,7 @@ lemma wideCospan.limitIsoPi_hom_comp_pi [Finite ι] (X : C) (j : ι) :
   rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]
 
 /-- Given an object `X : C`, the Čech nerve of the hom to the terminal object `X ⟶ ⊤_ C` is
-naturally isomorphic to a simplicial object sending `[n]` to `Xⁿ⁺¹` (when `C` is `G-Set`, this is
+naturally isomorphic to a simplicial object sending `⦋n⦌` to `Xⁿ⁺¹` (when `C` is `G-Set`, this is
 `EG`, the universal cover of the classifying space of `G`. -/
 def iso (X : C) : (Arrow.mk (terminal.from X)).cechNerve ≅ cechNerveTerminalFrom X :=
   NatIso.ofComponents (fun _ => wideCospan.limitIsoPi _ _) (fun {m n} f => by

Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

@@ -131,11 +131,11 @@ theorem postComp_φ : (f.postComp h).φ = f.φ ≫ h := by
 /-- A `MorphComponents` can be precomposed with a morphism of simplicial objects. -/
 @[simps]
 def preComp : MorphComponents X' n Z where
-  a := g.app (op [n + 1]) ≫ f.a
-  b i := g.app (op [n]) ≫ f.b i
+  a := g.app (op ⦋n + 1⦌) ≫ f.a
+  b i := g.app (op ⦋n⦌) ≫ f.b i
 
 @[simp]
-theorem preComp_φ : (f.preComp g).φ = g.app (op [n + 1]) ≫ f.φ := by
+theorem preComp_φ : (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ := by
   unfold φ preComp
   simp only [PInfty_f, comp_add]
   congr 1

Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -17,7 +17,7 @@ the subcomplex generated by the images of all `X.σ i`.
 
 In this file, we obtain `degeneracy_comp_P_infty` which states that
 if `X : SimplicialObject C` with `C` a preadditive category,
-`θ : [n] ⟶ Δ'` is a non injective map in `SimplexCategory`, then
+`θ : ⦋n⦌ ⟶ Δ'` is a non injective map in `SimplexCategory`, then
 `X.map θ.op ≫ P_infty.f n = 0`. It follows from the more precise
 statement vanishing statement `σ_comp_P_eq_zero` for the `P q`.
 
@@ -117,7 +117,7 @@ theorem σ_comp_PInfty (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) :
 
 @[reassoc]
 theorem degeneracy_comp_PInfty (X : SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory}
-    (θ : ([n] : SimplexCategory) ⟶ Δ') (hθ : ¬Mono θ) : X.map θ.op ≫ PInfty.f n = 0 := by
+    (θ : ⦋n⦌ ⟶ Δ') (hθ : ¬Mono θ) : X.map θ.op ≫ PInfty.f n = 0 := by
   rw [SimplexCategory.mono_iff_injective] at hθ
   cases n
   · exfalso

Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean

@@ -57,7 +57,7 @@ theorem iff {j : ℕ} {i : Fin (j + 2)} : Isδ₀ (SimplexCategory.δ i) ↔ i =
   · rintro rfl
     exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
 
-theorem eq_δ₀ {n : ℕ} {i : ([n] : SimplexCategory) ⟶ [n + 1]} [Mono i] (hi : Isδ₀ i) :
+theorem eq_δ₀ {n : ℕ} {i : ⦋n⦌ ⟶ ⦋n + 1⦌} [Mono i] (hi : Isδ₀ i) :
     i = SimplexCategory.δ 0 := by
   obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono i
   rw [iff] at hi
@@ -217,7 +217,7 @@ def obj (K : ChainComplex C ℕ) : SimplicialObject C where
 /-- By construction, the simplicial `Γ₀.obj K` is equipped with a splitting. -/
 def splitting (K : ChainComplex C ℕ) : SimplicialObject.Splitting (Γ₀.obj K) where
   N n := K.X n
-  ι n := Sigma.ι (Γ₀.Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))
+  ι n := Sigma.ι (Γ₀.Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))
   isColimit' Δ := IsColimit.ofIsoColimit (colimit.isColimit _) (Cofan.ext (Iso.refl _) (by
       intro A
       dsimp [Splitting.cofan']
@@ -311,7 +311,7 @@ def Γ₂ : Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C) :=
 
 theorem HigherFacesVanish.on_Γ₀_summand_id (K : ChainComplex C ℕ) (n : ℕ) :
     @HigherFacesVanish C _ _ (Γ₀.obj K) _ n (n + 1)
-      (((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op [n + 1]))) := by
+      (((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n + 1⦌))) := by
   intro j _
   have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
   rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq; rotate_left
@@ -322,9 +322,9 @@ theorem HigherFacesVanish.on_Γ₀_summand_id (K : ChainComplex C ℕ) (n : ℕ)
 
 @[reassoc (attr := simp)]
 theorem PInfty_on_Γ₀_splitting_summand_eq_self (K : ChainComplex C ℕ) {n : ℕ} :
-    ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op [n])) ≫
+    ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
       (PInfty : K[Γ₀.obj K] ⟶ _).f n =
-      ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op [n])) := by
+      ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
   rw [PInfty_f]
   rcases n with _|n
   · simpa only [P_f_0_eq] using comp_id _

Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

@@ -149,7 +149,7 @@ def N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
 @[simp]
 theorem N₂Γ₂_inv_app_f_f (X : Karoubi (ChainComplex C ℕ)) (n : ℕ) :
     (N₂Γ₂.inv.app X).f.f n =
-      X.p.f n ≫ ((Γ₀.splitting X.X).cofan _).inj (Splitting.IndexSet.id (op [n])) := by
+      X.p.f n ≫ ((Γ₀.splitting X.X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
   dsimp [N₂Γ₂]
   simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
     Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,

Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean

@@ -138,7 +138,7 @@ theorem Hσ_eq_zero (q : ℕ) : (Hσ q : K[X] ⟶ K[X]).f 0 = 0 := by
 
 /-- The maps `hσ' q n m hnm` are natural on the simplicial object -/
 theorem hσ'_naturality (q : ℕ) (n m : ℕ) (hnm : c.Rel m n) {X Y : SimplicialObject C} (f : X ⟶ Y) :
-    f.app (op [n]) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op [m]) := by
+    f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌) := by
   have h : n + 1 = m := hnm
   subst h
   simp only [hσ', eqToHom_refl, comp_id]

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -34,7 +34,7 @@ namespace DoldKan
 variable {C : Type*} [Category C] [Preadditive C]
 
 theorem PInfty_comp_map_mono_eq_zero (X : SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory}
-    (i : Δ' ⟶ [n]) [hi : Mono i] (h₁ : Δ'.len ≠ n) (h₂ : ¬Isδ₀ i) :
+    (i : Δ' ⟶ ⦋n⦌) [hi : Mono i] (h₁ : Δ'.len ≠ n) (h₂ : ¬Isδ₀ i) :
     PInfty.f n ≫ X.map i.op = 0 := by
   induction' Δ' using SimplexCategory.rec with m
   obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
@@ -196,11 +196,11 @@ theorem identity_N₂_objectwise (P : Karoubi (SimplicialObject C)) :
     (N₂Γ₂.inv.app (N₂.obj P) : N₂.obj P ⟶ N₂.obj (Γ₂.obj (N₂.obj P))) ≫
     N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P) := by
   ext n
-  have eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op [n]) ≫
-      ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op [n])) := by
+  have eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫
+      ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
     simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
-  have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op [n])) ≫
-      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op [n]) := by
+  have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
+      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) := by
     dsimp
     rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
     dsimp

Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

@@ -36,14 +36,14 @@ instance : (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)).Reflects
   ⟨fun {X Y} f => by
     intro
     -- restating the result in a way that allows induction on the degree n
-    suffices ∀ n : ℕ, IsIso (f.app (op [n])) by
+    suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌)) by
       haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
       apply NatIso.isIso_of_isIso_app
     -- restating the assumption in a more practical form
     have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
     have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
     have h₃ := fun n =>
-      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op [n]))
+      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
     simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
       AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃
     -- we have to construct an inverse to f in degree n, by induction on n
@@ -60,7 +60,7 @@ instance : (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)).Reflects
     | succ n hn =>
       haveI := hn
       use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
-              b := fun i => inv (f.app (op [n])) ≫ X.σ i }
+              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
       simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
         PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
         SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]⟩

Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

@@ -71,12 +71,12 @@ theorem QInfty_f (n : ℕ) : (QInfty.f n : X _[n] ⟶ X _[n]) = (Q n).f n :=
 
 @[reassoc (attr := simp)]
 theorem PInfty_f_naturality (n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
-    f.app (op [n]) ≫ PInfty.f n = PInfty.f n ≫ f.app (op [n]) :=
+    f.app (op ⦋n⦌) ≫ PInfty.f n = PInfty.f n ≫ f.app (op ⦋n⦌) :=
   P_f_naturality n n f
 
 @[reassoc (attr := simp)]
 theorem QInfty_f_naturality (n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
-    f.app (op [n]) ≫ QInfty.f n = QInfty.f n ≫ f.app (op [n]) :=
+    f.app (op ⦋n⦌) ≫ QInfty.f n = QInfty.f n ≫ f.app (op ⦋n⦌) :=
   Q_f_naturality n n f
 
 @[reassoc (attr := simp)]
@@ -157,7 +157,7 @@ computes `PInfty` for the associated object in `SimplicialObject (Karoubi C)`
 in terms of `PInfty` for `Y.X : SimplicialObject C` and `Y.p`. -/
 theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
     ((PInfty : K[(karoubiFunctorCategoryEmbedding _ _).obj Y] ⟶ _).f n).f =
-      Y.p.app (op [n]) ≫ (PInfty : K[Y.X] ⟶ _).f n := by
+      Y.p.app (op ⦋n⦌) ≫ (PInfty : K[Y.X] ⟶ _).f n := by
   -- We introduce P_infty endomorphisms P₁, P₂, P₃, P₄ on various objects Y₁, Y₂, Y₃, Y₄.
   let Y₁ := (karoubiFunctorCategoryEmbedding _ _).obj Y
   let Y₂ := Y.X
@@ -168,7 +168,7 @@ theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
   let P₃ : K[Y₃] ⟶ _ := PInfty
   let P₄ : K[Y₄] ⟶ _ := PInfty
   -- The statement of lemma relates P₁ and P₂.
-  change (P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
+  change (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
   -- The proof proceeds by obtaining relations h₃₂, h₄₃, h₁₄.
   have h₃₂ : (P₃.f n).f = P₂.f n := Karoubi.hom_ext_iff.mp (map_PInfty_f (toKaroubi C) Y₂ n)
   have h₄₃ : P₄.f n = P₃.f n := by
@@ -188,7 +188,7 @@ theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
   have eq := Karoubi.hom_ext_iff.mp (PInfty_f_naturality n π)
   simp only [Karoubi.comp_f] at eq
   dsimp [π] at eq
-  rw [← eq, app_idem_assoc Y (op [n])]
+  rw [← eq, app_idem_assoc Y (op ⦋n⦌)]
 
 end DoldKan