chore(category_theory): simps should not add hom lemmas (#18742)

kim-em · kim-em · commit 2efd2423f8d2 · 2023-04-08T11:36:43.000Z
`@[simps]` should not be used to simplify the `hom` field of a category instance. Very little needs to be changed when removing it. However the problem in leanprover-community/mathlib4#3244 with a proof by `simp` failing seems to be implicated by this problem. If we remove the `@[simps]` generated lemma for `Hom` there, the original proof works (although is extremely slow). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
diff --git a/src/category_theory/category/basic.lean b/src/category_theory/category/basic.lean
@@ -85,6 +85,8 @@ extends quiver.{v+1} obj : Type (max u (v+1)) :=
 notation `𝟙` := category_struct.id -- type as \b1
 infixr ` ≫ `:80 := category_struct.comp -- type as \gg
 
+initialize_simps_projections category_struct (-to_quiver_hom)
+
 /--
 The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
@@ -122,8 +124,8 @@ abbreviation small_category (C : Type u) : Type (u+1) := category.{u} C
 section
 variables {C : Type u} [category.{v} C] {X Y Z : C}
 
-initialize_simps_projections category (to_category_struct_to_quiver_hom → hom,
-  to_category_struct_comp → comp, to_category_struct_id → id, -to_category_struct)
+initialize_simps_projections category
+  (to_category_struct_comp → comp, to_category_struct_id → id, -to_category_struct)
 
 /-- postcompose an equation between morphisms by another morphism -/
 lemma eq_whisker {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : f ≫ h = g ≫ h :=
diff --git a/src/category_theory/fin_category.lean b/src/category_theory/fin_category.lean
@@ -60,15 +60,14 @@ noncomputable def obj_as_type_equiv : obj_as_type α ≌ α :=
 /-- A fin_category `α` is equivalent to a fin_category with in `Type`. -/
 @[nolint unused_arguments] abbreviation as_type : Type := fin (fintype.card α)
 
-@[simps hom id comp (lemmas_only)] noncomputable
+@[simps id comp (lemmas_only)] noncomputable
 instance category_as_type : small_category (as_type α) :=
 { hom := λ i j, fin (fintype.card (@quiver.hom (obj_as_type α) _ i j)),
   id := λ i, fintype.equiv_fin _ (𝟙 i),
   comp := λ i j k f g, fintype.equiv_fin _
     ((fintype.equiv_fin _).symm f ≫ (fintype.equiv_fin _).symm g) }
 
-local attribute [simp] category_as_type_hom category_as_type_id
-  category_as_type_comp
+local attribute [simp] category_as_type_id category_as_type_comp
 
 /-- The "identity" functor from `as_type α` to `obj_as_type α`. -/
 @[simps] noncomputable def as_type_to_obj_as_type : as_type α ⥤ obj_as_type α :=
diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean
@@ -45,6 +45,11 @@ class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=
 restate_axiom groupoid.inv_comp'
 restate_axiom groupoid.comp_inv'
 
+
+initialize_simps_projections groupoid (-to_category_to_category_struct_to_quiver_hom,
+  to_category_to_category_struct_comp → comp, to_category_to_category_struct_id → id,
+  -to_category_to_category_struct, -to_category)
+
 /--
 A `large_groupoid` is a groupoid
 where the objects live in `Type (u+1)` while the morphisms live in `Type u`.
diff --git a/src/category_theory/monoidal/braided.lean b/src/category_theory/monoidal/braided.lean
@@ -221,6 +221,9 @@ class symmetric_category (C : Type u) [category.{v} C] [monoidal_category.{v} C]
 restate_axiom symmetric_category.symmetry'
 attribute [simp,reassoc] symmetric_category.symmetry
 
+initialize_simps_projections symmetric_category
+  (to_braided_category_braiding → braiding, -to_braided_category)
+
 variables (C : Type u₁) [category.{v₁} C] [monoidal_category C] [braided_category C]
 variables (D : Type u₂) [category.{v₂} D] [monoidal_category D] [braided_category D]
 variables (E : Type u₃) [category.{v₃} E] [monoidal_category E] [braided_category E]
diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean
@@ -373,7 +373,7 @@ instance : has_add (P ⟶ Q) :=
 instance : add_comm_group (P ⟶ Q) :=
 function.injective.add_comm_group (λ (f : Sheaf.hom P Q), f.1)
   (λ _ _ h, Sheaf.hom.ext _ _ h) rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
-  (λ _ _, by { dsimp at *, ext, simpa [*] }) (λ _ _, by { dsimp at *, ext, simpa [*] })
+  (λ _ _, by { ext, simpa [*] }) (λ _ _, by { ext, simpa [*] })
 
 instance : preadditive (Sheaf J A) :=
 { hom_group := λ P Q, infer_instance,
