chore(AlgebraicTopology): making SimplexCategory a one-field structure (#37734)

Author: joelriou

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -152,7 +152,6 @@ def cechNerveEquiv (X : SimplicialObject.Augmented C) (F : Arrow C) :
     ext x : 2
     · refine WidePullback.hom_ext _ _ _ (fun j => ?_) ?_
       · simp
-        rfl
       · simpa using congr_app A.w.symm x
     · simp
 

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -44,7 +44,6 @@ theorem PInfty_comp_map_mono_eq_zero (X : SimplicialObject C) {n : ℕ} {Δ' : S
   obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
         rw [← h] at h₁
         exact h₁ rfl)
-  simp only [len_mk] at hk
   rcases k with _ | k
   · change n = m + 1 at hk
     subst hk
@@ -97,7 +96,6 @@ theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ'
   · have h' : n' = n + 1 := hi.left
     subst h'
     simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
-    dsimp
     rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
     simp only [Preadditive.comp_sum]
     rw [Finset.sum_eq_single (0 : Fin (n + 2))]

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

@@ -303,7 +303,6 @@ theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
     δ (Fin.castSucc i) ≫ σ i = 𝟙 ⦋n⦌ := by
   rcases i with ⟨i, hi⟩
   ext ⟨j, hj⟩
-  simp? at hj says simp only [len_mk] at hj
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
   simp only [Fin.lt_def, Fin.dite_val, Fin.ite_val, Fin.val_pred]
   split_ifs
@@ -728,10 +727,8 @@ theorem iso_eq_iso_refl {x : SimplexCategory} (e : x ≅ x) : e = Iso.refl x :=
   have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)
   have eq₂ :=
     Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
-  ext : 2
-  convert congr_arg (fun φ => (OrderEmbedding.toOrderHom φ)) (eq₁.trans eq₂.symm)
-  ext i : 2
-  rfl
+  ext : 4
+  exact DFunLike.congr_fun (eq₁.trans eq₂.symm) _
 
 theorem eq_id_of_isIso {x : SimplexCategory} (f : x ⟶ x) [IsIso f] : f = 𝟙 _ :=
   congr_arg (fun φ : _ ≅ _ => φ.hom) (iso_eq_iso_refl (asIso f))

Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

@@ -12,16 +12,14 @@ public import Mathlib.Util.Superscript
 
 /-! # The simplex category
 
-We construct a skeletal model of the simplex category, with objects `ℕ` and the
-morphisms `n ⟶ m` being the monotone maps from `Fin (n + 1)` to `Fin (m + 1)`.
+We construct a skeletal model of the simplex category, with an object `⦋n⦌` for each `n : ℕ`, and
+morphisms `⦋n⦌ ⟶ ⦋m⦌` identify to monotone maps from `Fin (n + 1)` to `Fin (m + 1)`.
 
 In `Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean`, we show that this category
 is equivalent to `NonemptyFinLinOrd`.
 
 ## Remarks
 
-The definitions `SimplexCategory` and `SimplexCategory.Hom` are marked as irreducible.
-
 We provide the following functions to work with these objects:
 1. `SimplexCategory.mk` creates an object of `SimplexCategory` out of a natural number.
   Use the notation `⦋n⦌` in the `Simplicial` locale.
@@ -46,47 +44,29 @@ universe v
 open CategoryTheory
 
 /-- The simplex category:
-* objects are natural numbers `n : ℕ`
-* morphisms from `n` to `m` are monotone functions `Fin (n+1) → Fin (m+1)`
+* for each `n : ℕ`, there is an object `⦋n⦌`;
+* morphisms `⦋n⦌ ⟶ ⦋m⦌` are monotone functions `Fin (n+1) → Fin (m+1)`
 -/
-def SimplexCategory :=
-  ℕ
+@[ext]
+structure SimplexCategory : Type where
+  /-- Constructor `ℕ → SimplexCategory`. -/
+  mk ::
+  /-- The length of an object in `SimplexCategory` -/
+  len : ℕ
 
 namespace SimplexCategory
 
--- The definition of `SimplexCategory` is made irreducible below.
-/-- Interpret a natural number as an object of the simplex category. -/
-def mk (n : ℕ) : SimplexCategory :=
-  n
-
 /-- the `n`-dimensional simplex can be denoted `⦋n⦌` -/
 scoped[Simplicial] notation "⦋" n "⦌" => SimplexCategory.mk n
 
--- TODO: Make `len` irreducible.
-/-- The length of an object of `SimplexCategory`. -/
-def len (n : SimplexCategory) : ℕ :=
-  n
-
-@[ext]
-theorem ext (a b : SimplexCategory) : a.len = b.len → a = b :=
-  id
-
-attribute [irreducible] SimplexCategory
-
 open Simplicial
 
-@[simp]
-theorem len_mk (n : ℕ) : ⦋n⦌.len = n :=
-  rfl
+theorem len_mk (n : ℕ) : ⦋n⦌.len = n := rfl
 
 @[simp]
 theorem mk_len (n : SimplexCategory) : ⦋n.len⦌ = n :=
   rfl
 
-/-- A recursor for `SimplexCategory`. Use it as `induction Δ using SimplexCategory.rec`. -/
-protected def rec {F : SimplexCategory → Sort*} (h : ∀ n : ℕ, F ⦋n⦌) : ∀ X, F X := fun n =>
-  h n.len
-
 /-- Morphisms in the `SimplexCategory`. -/
 protected def Hom (a b : SimplexCategory) :=
   Fin (a.len + 1) →o Fin (b.len + 1)
@@ -106,8 +86,6 @@ theorem ext' {a b : SimplexCategory} (f g : SimplexCategory.Hom a b) :
     f.toOrderHom = g.toOrderHom → f = g :=
   id
 
-attribute [irreducible] SimplexCategory.Hom
-
 @[simp]
 theorem mk_toOrderHom {a b : SimplexCategory} (f : SimplexCategory.Hom a b) : mk f.toOrderHom = f :=
   rfl
@@ -134,6 +112,8 @@ def comp {a b c : SimplexCategory} (f : SimplexCategory.Hom b c) (g : SimplexCat
 
 end Hom
 
+attribute [irreducible] SimplexCategory.Hom
+
 instance smallCategory : SmallCategory.{0} SimplexCategory where
   Hom n m := SimplexCategory.Hom n m
   id _ := SimplexCategory.Hom.id _

Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean

@@ -62,7 +62,7 @@ lemma rev_map_σ {n : ℕ} (i : Fin (n + 1)) :
 set_option backward.isDefEq.respectTransparency false in
 /-- The functor `SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory`
 is a covariant involution. -/
-@[simps!]
+@[simps! hom_app inv_app]
 def revCompRevIso : rev ⋙ rev ≅ 𝟭 _ :=
   NatIso.ofComponents (fun _ ↦ Iso.refl _)
 

Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean

@@ -118,24 +118,26 @@ private lemma comm_succ (n : ℕ) :
     grind
   have h₃ : Disjoint (Finset.disjUnion _ _ h₂) {(0, 0), (Fin.last _, Fin.last _)} := by
     rw [Finset.disjoint_iff_ne]
+    simp only [Finset.mem_insert, forall_eq_or_imp, Prod.forall]
+    rintro ⟨a, _⟩ ⟨b, _⟩
+    simp
     grind
   have h₄ : Disjoint (Finset.disjUnion _ _ h₁) (Finset.disjUnion _ _ h₃) := by
     rw [Finset.disjoint_iff_ne]
     simp only [Finset.compl_filter, not_lt, Finset.disjUnion_eq_union, Finset.mem_union,
       Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and, Prod.exists, ne_eq,
       Finset.mem_insert, Finset.mem_singleton, Prod.forall, Prod.mk.injEq, not_and,
       S, γ₁, γ₂, γ₃, γ₄]
-    rintro _ _ (⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩ | ⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩) _ _
+    rintro ⟨a, _⟩ ⟨b, _⟩ (⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩ | ⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩) _ _
       ((⟨⟨i, _⟩, h₄, h₅⟩ | ⟨⟨i, _⟩, h₄, h₅⟩) | (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)) <;>
-      simp at h₁ h₂ h₃ <;> grind
+        simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢ <;> grind
   have H : (Finset.disjUnion _ _ h₁)ᶜ = Finset.disjUnion _ _ h₃ :=
     Finset.compl_eq_of_disjoint_of_card_add_eq h₄ (by
       rw [Finset.card_disjUnion, Finset.card_disjUnion, Finset.card_disjUnion,
         Finset.card_image_of_injective _ hγ₁, Finset.card_image_of_injective _ hγ₂,
         Finset.card_image_of_injective _ hγ₃, Finset.card_image_of_injective _ hγ₄]
-      simp only [Finset.card_compl_add_card, Fintype.card_prod, Fintype.card_fin,
-        Finset.card_univ]
-      grind)
+      simp
+      lia)
   rw [eq₁, eq₂, ← S.sum_add_sum_compl, eq₃, eq₄,
     neg_add_rev, neg_neg, neg_neg, ← Finset.sum_disjUnion h₁,
     ← (Finset.disjUnion _ _ h₁).sum_add_sum_compl, neg_add,

Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

@@ -137,8 +137,7 @@ lemma hσ'₁ (x : X _⦋1⦌₂) :
 
 /-- Auxiliary definition for `SSet.Truncated.liftOfStrictSegal`. -/
 def app (n : (SimplexCategory.Truncated 2)ᵒᵖ) : X.obj n ⟶ Y.obj n := by
-  obtain ⟨n, hn⟩ := n
-  induction n using SimplexCategory.rec with | _ n
+  obtain ⟨⟨n⟩, hn⟩ := n
   match n with
   | 0 => exact f₀
   | 1 => exact f₁

Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean

@@ -42,7 +42,7 @@ lemma mem_range_nerve_σ_iff (s : (nerve X) _⦋n + 1⦌) (i : Fin (n + 1)) :
       rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
         Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
     · simp only [not_lt] at h₁
-      grind [SimplexCategory.len_mk, → Fin.succAbove_of_castSucc_lt,
+      grind [→ Fin.succAbove_of_castSucc_lt,
         → Fin.predAbove_of_le_castSucc, Fin.castSucc_castPred, Fin.castPred_castSucc,
         Fin.succAbove_castSucc_self, → LE.le.lt_or_eq]
 
@@ -64,7 +64,7 @@ lemma mem_nerve_nonDegenerate_iff_strictMono (s : (nerve X) _⦋n⦌) :
     apply exists_congr
     intro i
     have := s.monotone i.castSucc_le_succ
-    grind [SimplexCategory.len_mk, lt_self_iff_false, LE.le.lt_or_eq]
+    grind [lt_self_iff_false, LE.le.lt_or_eq]
 
 lemma mem_nerve_nonDegenerate_iff_injective (s : (nerve X) _⦋n⦌) :
     s ∈ (nerve X).nonDegenerate n ↔ Function.Injective s.obj := by

Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean

@@ -75,10 +75,7 @@ variable (p q) in
 /-- The binary product `Δ[p] ⊗ Δ[q]` identifies to the nerve
 of `ULift (Fin (p + 1) × Fin (q + 1))`. -/
 def isoNerve : Δ[p] ⊗ Δ[q] ≅ nerve (ULift.{u} (Fin (p + 1) × Fin (q + 1))) :=
-  NatIso.ofComponents (fun d ↦ Equiv.toIso (by
-    obtain ⟨d⟩ := d
-    induction d using SimplexCategory.rec with | _ d
-    exact objEquiv.trans
+  NatIso.ofComponents (fun ⟨⟨d⟩⟩ ↦ Equiv.toIso (objEquiv.trans
       { toFun f := (ULift.orderIso.symm.monotone.comp f.monotone).functor
         invFun s := ULift.orderIso.toOrderEmbedding.toOrderHom.comp ⟨_, s.monotone⟩ }))
 

Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

@@ -59,9 +59,9 @@ noncomputable def nonDegenerateEquiv₁ :
       obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by
         rintro rfl
         have := DFunLike.congr_fun hs 0
-        simp only [orderHomOfSimplex_coe, OrderHom.id_coe, id_eq, Fin.ext_iff,
+        simp only [orderHomOfSimplex_coe,
           stdSimplex.objMk₁_of_le_castSucc (0 : Fin (p + 3)) 0 (by simp)] at this
-        lia)
+        simp at this)
       obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
       · exact ⟨i, nonDegenerate_ext₂ rfl rfl⟩
       · have := DFunLike.congr_fun hs (Fin.last _)