chore: refactor of concrete categories (#3900)

I think the ports
* #2902 (MonCat)
* #3036 (GroupCat)
* #3260 (ModuleCat)

didn't quite get things right, and also have some variation between them. This PR tries to straighten things out.

Major changes:
* Have the coercion to type be via `X.\a`, and put attribute `@[coe]` on this.
* Make sure the coercion from morphisms to functions means that simp lemmas about the underlying bundled morphisms apply directly.
  * This means we drop lemmas like
  ```
  lemma Hom.map_mul {X Y : MonCat} (f : X ⟶ Y) (x y : X) : ((forget MonCat).map f) (x * y) = f x * f y
   ```
   * But at the expense of adding lemmas like
   ```
   lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
   ```

Overall I'm pretty happy, and it allows me to unstick the long stuck #3105.

This is not everything I want to do to refactor these files, but once I was satisfied that I can move forward with RingCat, I want to get this merged so we can unblock porting progress. I'll promise to come back to this soon! :-)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Mathlib/Algebra/Category/GroupCat/EpiMono.lean

@@ -303,7 +303,6 @@ theorem agree : f.range.carrier = { x | h x = g x } := by
         simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m)]
         congr
         rw [leftCoset_assoc _ (f a) y]
-        rfl
       · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
         simp only [leftCoset_assoc]
     · rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
@@ -324,7 +323,6 @@ theorem comp_eq : (f ≫ show B ⟶ GroupCat.of SX' from g) = f ≫ show B ⟶ G
   have : f a ∈ { b | h b = g b } := by
     rw [←agree]
     use a
-    rfl
   rw [this]
 #align Group.surjective_of_epi_auxs.comp_eq GroupCat.SurjectiveOfEpiAuxs.comp_eq
 
@@ -353,7 +351,7 @@ theorem surjective_of_epi [Epi f] : Function.Surjective f := by
 #align Group.surjective_of_epi GroupCat.surjective_of_epi
 
 theorem epi_iff_surjective : Epi f ↔ Function.Surjective f :=
-  ⟨fun _ => surjective_of_epi f, ConcreteCategory.epi_of_surjective _⟩
+  ⟨fun _ => surjective_of_epi f, ConcreteCategory.epi_of_surjective f⟩
 #align Group.epi_iff_surjective GroupCat.epi_iff_surjective
 
 theorem epi_iff_range_eq_top : Epi f ↔ f.range = ⊤ :=
@@ -454,8 +452,6 @@ theorem epi_iff_range_eq_top : Epi f ↔ f.range = ⊤ :=
 @[to_additive]
 theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by
   rw [epi_iff_range_eq_top, MonoidHom.range_top_iff_surjective]
-  -- Porting note: extra rfl forces the issue
-  rfl
 #align CommGroup.epi_iff_surjective CommGroupCat.epi_iff_surjective
 #align AddCommGroup.epi_iff_surjective AddCommGroupCat.epi_iff_surjective
 
@@ -474,4 +470,3 @@ instance forget_commGroupCat_preserves_epi : (forget CommGroupCat).PreservesEpim
 end CommGroupCat
 
 end
-

Mathlib/Algebra/Category/GroupCat/Zero.lean

@@ -32,7 +32,7 @@ theorem isZero_of_subsingleton (G : GroupCat) [Subsingleton G] : IsZero G := by
   refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
   · ext x
     have : x = 1 := Subsingleton.elim _ _
-    rw [this, Hom.map_one, Hom.map_one]
+    rw [this, map_one, map_one]
   · ext
     apply Subsingleton.elim
 set_option linter.uppercaseLean3 false in
@@ -53,7 +53,7 @@ theorem isZero_of_subsingleton (G : CommGroupCat) [Subsingleton G] : IsZero G :=
   refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
   · ext x
     have : x = 1 := Subsingleton.elim _ _
-    rw [this, Hom.map_one, Hom.map_one]
+    rw [this, map_one, map_one]
   · ext
     apply Subsingleton.elim
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -30,6 +30,8 @@ To construct an object in the category of `R`-modules from a type `M` with an in
 
 Similarly, there is a coercion from morphisms in `Module R` to linear maps.
 
+Porting note: the next two paragraphs should be revised.
+
 Unfortunately, Lean is not smart enough to see that, given an object `M : Module R`, the expression
 `of R M`, where we coerce `M` to the carrier type, is definitionally equal to `M` itself.
 This means that to go the other direction, i.e., from linear maps/equivalences to (iso)morphisms
@@ -85,7 +87,7 @@ namespace ModuleCat
 instance : CoeSort (ModuleCat.{v} R) (Type v) :=
   ⟨ModuleCat.carrier⟩
 
-attribute [-instance] Ring.toNonAssocRing
+attribute [coe] ModuleCat.carrier
 
 instance moduleCategory : Category (ModuleCat.{v} R) where
   Hom M N := M →ₗ[R] N
@@ -103,7 +105,7 @@ instance {M N : ModuleCat.{v} R} : FunLike (M ⟶ N) M (fun _ => N) :=
   ⟨fun f => f.toFun, fun _ _ h => LinearMap.ext (congr_fun h)⟩
 
 instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R) where
-  Forget :=
+  forget :=
     { obj := fun R => R
       map := fun f => f.toFun }
   forget_faithful := ⟨fun h => LinearMap.ext (fun x => by
@@ -114,13 +116,13 @@ set_option linter.uppercaseLean3 false in
 
 -- porting note: added to ease automation
 @[ext]
-lemma hom_ext {M N : ModuleCat.{v} R} (f₁ f₂ : M ⟶ N) (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
+lemma ext {M N : ModuleCat.{v} R} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
   FunLike.ext _ _ h
 
 instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGroupCat where
   forget₂ :=
     { obj := fun M => AddCommGroupCat.of M
-      map := fun f => LinearMap.toAddMonoidHom f }
+      map := fun f => AddCommGroupCat.ofHom f.toAddMonoidHom }
 set_option linter.uppercaseLean3 false in
 #align Module.has_forget_to_AddCommGroup ModuleCat.hasForgetToAddCommGroup
 
@@ -133,14 +135,18 @@ def of (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat R :=
 set_option linter.uppercaseLean3 false in
 #align Module.of ModuleCat.of
 
--- porting note: remove simp attribute because it makes the linter complain
+@[simp]
 theorem forget₂_obj (X : ModuleCat R) :
     (forget₂ (ModuleCat R) AddCommGroupCat).obj X = AddCommGroupCat.of X :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Module.forget₂_obj ModuleCat.forget₂_obj
 
-@[simp 900]
+-- Porting note: the simpNF linter correctly doesn't like this.
+-- I'm not sure what this is for, actually.
+-- If it is really needed, better might be a simp lemma that says
+-- `AddCommGroupCat.of (ModuleCat.of R X) = AddCommGroupCat.of X`.
+-- @[simp 900]
 theorem forget₂_obj_moduleCat_of (X : Type v) [AddCommGroup X] [Module R X] :
     (forget₂ (ModuleCat R) AddCommGroupCat).obj (of R X) = AddCommGroupCat.of X :=
   rfl
@@ -154,6 +160,8 @@ theorem forget₂_map (X Y : ModuleCat R) (f : X ⟶ Y) :
 set_option linter.uppercaseLean3 false in
 #align Module.forget₂_map ModuleCat.forget₂_map
 
+-- Porting note: TODO: `ofHom` and `asHom` are duplicates!
+
 /-- Typecheck a `LinearMap` as a morphism in `Module R`. -/
 def ofHom {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y]
     [Module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y :=
@@ -265,8 +273,6 @@ scoped[ModuleCat] notation "↿" f:1024 => ModuleCat.asHomLeft f
 
 section
 
-attribute [-instance] Ring.toNonAssocRing
-
 /-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s. -/
 @[simps]
 def LinearEquiv.toModuleIso {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁}

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -39,9 +39,7 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
   invFun φ := φ.app (ModuleCat.of R R) (1 : R)
   left_inv := by
     intro r
-    dsimp
-    erw [AddCommGroupCat.ofHom_apply]
-    simp only [DistribMulAction.toAddMonoidHom_apply, smul_eq_mul, mul_one]
+    simp
   right_inv := by
     intro φ
     apply NatTrans.ext