feat(AlgebraicTopology): basic missing lemmas about the simplex category (#31248)

Author: joelriou

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

@@ -26,7 +26,7 @@ open Simplicial CategoryTheory Limits
 
 namespace SimplexCategory
 
-instance {n m : ℕ} : DecidableEq (⦋n⦌ ⟶ ⦋m⦌) := fun a b =>
+instance {n m : SimplexCategory} : DecidableEq (n ⟶ m) := fun a b =>
   decidable_of_iff (a.toOrderHom = b.toOrderHom) SimplexCategory.Hom.ext_iff.symm
 
 section Init
@@ -145,6 +145,8 @@ lemma mkOfSucc_homToOrderHom_zero {n} (i : Fin n) :
 lemma mkOfSucc_homToOrderHom_one {n} (i : Fin n) :
     DFunLike.coe (F := Fin 2 →o Fin (n + 1)) (Hom.toOrderHom (mkOfSucc i)) 1 = i.succ := rfl
 
+@[simp]
+lemma mkOfSucc_eq_id : mkOfSucc (0 : Fin 1) = 𝟙 _ := by decide
 
 /-- The morphism `⦋2⦌ ⟶ ⦋n⦌` that picks out a specified composite of morphisms in `Fin (n+1)`. -/
 def mkOfLeComp {n} (i j k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) :
@@ -382,6 +384,10 @@ theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
         (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
         (Fin.succ_le_castSucc_iff.mpr h)]
 
+lemma δ_zero_eq_const : δ (0 : Fin 2) = const _ _ 1 := by decide
+
+lemma δ_one_eq_const : δ (1 : Fin 2) = const _ _ 0 := by decide
+
 /--
 If `f : ⦋m⦌ ⟶ ⦋n+1⦌` is a morphism and `j` is not in the range of `f`,
 then `factor_δ f j` is a morphism `⦋m⦌ ⟶ ⦋n⦌` such that
@@ -454,6 +460,10 @@ lemma mkOfSucc_δ_eq {n : ℕ} {i : Fin n} {j : Fin (n + 2)}
     rw [Fin.succAbove_castSucc_self]
     rfl
 
+lemma mkOfSucc_one_eq_δ : mkOfSucc (1 : Fin 2) = δ 0 := by decide
+
+lemma mkOfSucc_zero_eq_δ : mkOfSucc (0 : Fin 2) = δ 2 := by decide
+
 theorem eq_of_one_to_two (f : ⦋1⦌ ⟶ ⦋2⦌) :
     (∃ i, f = (δ (n := 1) i)) ∨ ∃ a, f = SimplexCategory.const _ _ a := by
   have : f.toOrderHom 0 ≤ f.toOrderHom 1 := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)

Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

@@ -161,12 +161,9 @@ def homEquivFunctor {a b : SimplexCategory} :
   SimplexCategory.homEquivOrderHom.trans OrderHom.equivFunctor
 
 /-- The truncated simplex category. -/
-def Truncated (n : ℕ) :=
+abbrev Truncated (n : ℕ) :=
   ObjectProperty.FullSubcategory fun a : SimplexCategory => a.len ≤ n
 
-instance (n : ℕ) : SmallCategory.{0} (Truncated n) :=
-  ObjectProperty.FullSubcategory.category _
-
 namespace Truncated
 
 instance {n} : Inhabited (Truncated n) :=
@@ -214,6 +211,11 @@ abbrev Hom.tr {n : ℕ} {a b : SimplexCategory} (f : a ⟶ b)
     (⟨a, ha⟩ : Truncated n) ⟶ ⟨b, hb⟩ :=
   f
 
+@[simp]
+lemma Hom.tr_id {n : ℕ} (a : SimplexCategory) (ha : a.len ≤ n := by trunc) :
+    Hom.tr (𝟙 a) ha = 𝟙 _ := rfl
+
+@[reassoc]
 lemma Hom.tr_comp {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c)
     (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc)
     (hc : c.len ≤ n := by trunc) :

Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean

@@ -17,6 +17,9 @@ open Simplicial CategoryTheory
 
 namespace SimplexCategory.Truncated
 
+instance {d : ℕ} {n m : Truncated d} : DecidableEq (n ⟶ m) := fun a b =>
+  decidable_of_iff (a.toOrderHom = b.toOrderHom) SimplexCategory.Hom.ext_iff.symm
+
 /-- For `0 < n`, the inclusion functor from the `n`-truncated simplex category to the untruncated
 simplex category is initial. -/
 instance initial_inclusion {n : ℕ} [NeZero n] : (inclusion n).Initial := by
@@ -75,6 +78,11 @@ lemma δ₂_zero_comp_σ₂_one : δ₂ (0 : Fin 3) ≫ σ₂ 1 = σ₂ 0 ≫ δ
 lemma δ₂_one_comp_σ₂_zero {n} (hn := by decide) (hn' := by decide) :
     δ₂ (n := n) 1 hn hn' ≫ σ₂ 0 hn' hn = 𝟙 _ := SimplexCategory.δ_comp_σ_succ
 
+@[reassoc (attr := simp)]
+lemma δ₂_one_comp_σ₂_one {n} (hn := by decide) (hn' := by decide) :
+    δ₂ (n := n + 1) 1 hn hn' ≫ σ₂ 1 hn' hn = 𝟙 _ :=
+  SimplexCategory.δ_comp_σ_self (n := n + 1) (i := 1)
+
 @[reassoc (attr := simp)]
 lemma δ₂_two_comp_σ₂_one : δ₂ (2 : Fin 3) ≫ σ₂ 1 = 𝟙 _ :=
   SimplexCategory.δ_comp_σ_succ' (by decide)
@@ -83,6 +91,13 @@ lemma δ₂_two_comp_σ₂_one : δ₂ (2 : Fin 3) ≫ σ₂ 1 = 𝟙 _ :=
 lemma δ₂_two_comp_σ₂_zero : δ₂ (2 : Fin 3) ≫ σ₂ 0 = σ₂ 0 ≫ δ₂ 1 :=
   SimplexCategory.δ_comp_σ_of_gt' (by decide)
 
+lemma δ₂_one_eq_const : δ₂ (1 : Fin 2) = const _ _ 0 := by decide
+
+lemma δ₂_zero_eq_const : δ₂ (0 : Fin 2) = const _ _ 1 := by decide
+
+@[reassoc]
+lemma δ₂_zero_comp_δ₂_two : δ₂ (0 : Fin 2) ≫ δ₂ 2 = δ₂ 1 ≫ δ₂ 0 := by decide
+
 end Two
 
 end SimplexCategory.Truncated

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -92,10 +92,14 @@ variable (X : SimplicialObject C)
 def δ {n} (i : Fin (n + 2)) : X _⦋n + 1⦌ ⟶ X _⦋n⦌ :=
   X.map (SimplexCategory.δ i).op
 
+lemma δ_def {n} (i : Fin (n + 2)) : X.δ i = X.map (SimplexCategory.δ i).op := rfl
+
 /-- Degeneracy maps for a simplicial object. -/
 def σ {n} (i : Fin (n + 1)) : X _⦋n⦌ ⟶ X _⦋n + 1⦌ :=
   X.map (SimplexCategory.σ i).op
 
+lemma σ_def {n} (i : Fin (n + 1)) : X.σ i = X.map (SimplexCategory.σ i).op := rfl
+
 /-- The diagonal of a simplex is the long edge of the simplex. -/
 def diagonal {n : ℕ} : X _⦋n⦌ ⟶ X _⦋1⦌ := X.map ((SimplexCategory.diag n).op)
 

Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -115,6 +115,17 @@ abbrev trunc (n m : ℕ) (h : m ≤ n := by omega) :
     SSet.Truncated n ⥤ SSet.Truncated m :=
   SimplicialObject.Truncated.trunc (Type u) n m
 
+@[simp]
+lemma id_app {n : ℕ} (X : Truncated n) (d : (SimplexCategory.Truncated n)ᵒᵖ) :
+    NatTrans.app (𝟙 X) d = 𝟙 _ :=
+  rfl
+
+@[simp, reassoc]
+lemma comp_app {n : ℕ} {X Y Z : Truncated n} (f : X ⟶ Y) (g : Y ⟶ Z)
+    (d : (SimplexCategory.Truncated n)ᵒᵖ) :
+    (f ≫ g).app d = f.app d ≫ g.app d :=
+  rfl
+
 end Truncated
 
 /-- The truncation functor on simplicial sets. -/